Roots of unity and primitive roots of unity

We define roots of unity in the context of an arbitrary commutative monoid, as a subgroup of the group of units. We also define a predicate IsPrimitiveRoot on commutative monoids, expressing that an element is a primitive root of unity.

Main definitions

• rootsOfUnity n M, for n : ℕ is the subgroup of the units of a commutative monoid M consisting of elements x that satisfy x ^ n = 1.
• IsPrimitiveRoot ζ k: an element ζ is a primitive k-th root of unity if ζ ^ k = 1, and if l satisfies ζ ^ l = 1 then k ∣ l.
• primitiveRoots k R: the finset of primitive k-th roots of unity in an integral domain R.
• IsPrimitiveRoot.autToPow: the monoid hom that takes an automorphism of a ring to the power it sends that specific primitive root, as a member of (ZMod n)ˣ.

Main results

• rootsOfUnity.isCyclic: the roots of unity in an integral domain form a cyclic group.
• IsPrimitiveRoot.zmodEquivZPowers: ZMod k is equivalent to the subgroup generated by a primitive k-th root of unity.
• IsPrimitiveRoot.zpowers_eq: in an integral domain, the subgroup generated by a primitive k-th root of unity is equal to the k-th roots of unity.
• IsPrimitiveRoot.card_primitiveRoots: if an integral domain has a primitive k-th root of unity, then it has φ k of them.

Implementation details

It is desirable that rootsOfUnity is a subgroup, and it will mainly be applied to rings (e.g. the ring of integers in a number field) and fields. We therefore implement it as a subgroup of the units of a commutative monoid.

We have chosen to define rootsOfUnity n for n : ℕ and add a [NeZero n] typeclass assumption when we need n to be non-zero (which is the case for most interesting statements). Note that rootsOfUnity 0 M is the top subgroup of Mˣ (as the condition ζ^0 = 1 is satisfied for all units).

On the other hand, for primitive roots of unity, it is desirable to have a predicate not just on units, but directly on elements of the ring/field. For example, we want to say that exp (2 * pi * I / n) is a primitive n-th root of unity in the complex numbers, without having to turn that number into a unit first.

This creates a little bit of friction, but lemmas like IsPrimitiveRoot.isUnit and IsPrimitiveRoot.coe_units_iff should provide the necessary glue.

def rootsOfUnity (k : ℕ) (M : Type u_7) [CommMonoid M] : Subgroup Mˣ

rootsOfUnity k M is the subgroup of elements m : Mˣ that satisfy m ^ k = 1.

Equations

• rootsOfUnity k M = { carrier := {ζ : Mˣ | ζ ^ k = 1}, mul_mem' := ⋯, one_mem' := ⋯, inv_mem' := ⋯ }

@[simp]

theorem mem_rootsOfUnity {M : Type u_1} [CommMonoid M] (k : ℕ) (ζ : Mˣ) : ζ ∈ rootsOfUnity k M ↔ ζ ^ k = 1

theorem mem_rootsOfUnity' {M : Type u_1} [CommMonoid M] (k : ℕ) (ζ : Mˣ) : ζ ∈ rootsOfUnity k M ↔ ↑ζ ^ k = 1

A variant of mem_rootsOfUnity using ζ : M.

@[simp]

theorem rootsOfUnity_one (M : Type u_7) [CommMonoid M] : rootsOfUnity 1 M = ⊥

@[simp]

theorem rootsOfUnity_zero (M : Type u_7) [CommMonoid M] : rootsOfUnity 0 M = ⊤

theorem rootsOfUnity.coe_injective {M : Type u_1} [CommMonoid M] {n : ℕ} : Function.Injective fun (x : ↥(rootsOfUnity n M)) => ↑↑x

def rootsOfUnity.mkOfPowEq {M : Type u_1} [CommMonoid M] (ζ : M) {n : ℕ} [NeZero n] (h : ζ ^ n = 1) : ↥(rootsOfUnity n M)

Make an element of rootsOfUnity from a member of the base ring, and a proof that it has a positive power equal to one.

Equations

• rootsOfUnity.mkOfPowEq ζ h = ⟨Units.ofPowEqOne ζ n h ⋯, ⋯⟩

@[simp]

theorem rootsOfUnity.val_mkOfPowEq_coe {M : Type u_1} [CommMonoid M] (ζ : M) {n : ℕ} [NeZero n] (h : ζ ^ n = 1) : ↑↑(rootsOfUnity.mkOfPowEq ζ h) = ζ

@[simp]

theorem rootsOfUnity.coe_mkOfPowEq {M : Type u_1} [CommMonoid M] {ζ : M} {n : ℕ} [NeZero n] (h : ζ ^ n = 1) : ↑↑(rootsOfUnity.mkOfPowEq ζ h) = ζ

theorem rootsOfUnity_le_of_dvd {M : Type u_1} [CommMonoid M] {k : ℕ} {l : ℕ} (h : k ∣ l) : rootsOfUnity k M ≤ rootsOfUnity l M

theorem map_rootsOfUnity {M : Type u_1} {N : Type u_2} [CommMonoid M] [CommMonoid N] (f : Mˣ →* Nˣ) (k : ℕ) : Subgroup.map f (rootsOfUnity k M) ≤ rootsOfUnity k N

theorem rootsOfUnity.coe_pow {R : Type u_4} {k : ℕ} [CommMonoid R] (ζ : ↥(rootsOfUnity k R)) (m : ℕ) : ↑↑(ζ ^ m) = ↑↑ζ ^ m

def restrictRootsOfUnity {R : Type u_4} {S : Type u_5} {F : Type u_6} [CommMonoid R] [CommMonoid S] [FunLike F R S] [MonoidHomClass F R S] (σ : F) (n : ℕ) : ↥(rootsOfUnity n R) →* ↥(rootsOfUnity n S)

Restrict a ring homomorphism to the nth roots of unity.

Equations

• restrictRootsOfUnity σ n = { toFun := fun (ξ : ↥(rootsOfUnity n R)) => ⟨(Units.map ↑σ) ↑ξ, ⋯⟩, map_one' := ⋯, map_mul' := ⋯ }

@[simp]

theorem restrictRootsOfUnity_coe_apply {R : Type u_4} {S : Type u_5} {F : Type u_6} {k : ℕ} [CommMonoid R] [CommMonoid S] [FunLike F R S] [MonoidHomClass F R S] (σ : F) (ζ : ↥(rootsOfUnity k R)) : ↑↑((restrictRootsOfUnity σ k) ζ) = σ ↑↑ζ

def MulEquiv.restrictRootsOfUnity {R : Type u_4} {S : Type u_5} [CommMonoid R] [CommMonoid S] (σ : R ≃* S) (n : ℕ) : ↥(rootsOfUnity n R) ≃* ↥(rootsOfUnity n S)

Restrict a monoid isomorphism to the nth roots of unity.

Equations

• σ.restrictRootsOfUnity n = { toFun := ⇑(restrictRootsOfUnity σ n), invFun := ⇑(restrictRootsOfUnity σ.symm n), left_inv := ⋯, right_inv := ⋯, map_mul' := ⋯ }

@[simp]

theorem MulEquiv.restrictRootsOfUnity_coe_apply {R : Type u_4} {S : Type u_5} {k : ℕ} [CommMonoid R] [CommMonoid S] (σ : R ≃* S) (ζ : ↥(rootsOfUnity k R)) : ↑↑((σ.restrictRootsOfUnity k) ζ) = σ ↑↑ζ

@[simp]

theorem MulEquiv.restrictRootsOfUnity_symm {R : Type u_4} {S : Type u_5} {k : ℕ} [CommMonoid R] [CommMonoid S] (σ : R ≃* S) : (σ.restrictRootsOfUnity k).symm = σ.symm.restrictRootsOfUnity k

theorem mem_rootsOfUnity_iff_mem_nthRoots {R : Type u_4} {k : ℕ} [NeZero k] [CommRing R] [IsDomain R] {ζ : Rˣ} : ζ ∈ rootsOfUnity k R ↔ ↑ζ ∈ Polynomial.nthRoots k 1

def rootsOfUnityEquivNthRoots (R : Type u_4) (k : ℕ) [NeZero k] [CommRing R] [IsDomain R] : ↥(rootsOfUnity k R) ≃ { x : R // x ∈ Polynomial.nthRoots k 1 }

Equivalence between the k-th roots of unity in R and the k-th roots of 1.

This is implemented as equivalence of subtypes, because rootsOfUnity is a subgroup of the group of units, whereas nthRoots is a multiset.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem rootsOfUnityEquivNthRoots_apply {R : Type u_4} {k : ℕ} [NeZero k] [CommRing R] [IsDomain R] (x : ↥(rootsOfUnity k R)) : ↑((rootsOfUnityEquivNthRoots R k) x) = ↑↑x

@[simp]

theorem rootsOfUnityEquivNthRoots_symm_apply {R : Type u_4} {k : ℕ} [NeZero k] [CommRing R] [IsDomain R] (x : { x : R // x ∈ Polynomial.nthRoots k 1 }) : ↑↑((rootsOfUnityEquivNthRoots R k).symm x) = ↑x

instance rootsOfUnity.fintype (R : Type u_4) (k : ℕ) [NeZero k] [CommRing R] [IsDomain R] : Fintype ↥(rootsOfUnity k R)

Equations

• rootsOfUnity.fintype R k = Fintype.ofEquiv { x : R // x ∈ Polynomial.nthRoots k 1 } (rootsOfUnityEquivNthRoots R k).symm

instance rootsOfUnity.isCyclic (R : Type u_4) (k : ℕ) [NeZero k] [CommRing R] [IsDomain R] : IsCyclic ↥(rootsOfUnity k R)

Equations

• ⋯ = ⋯

theorem card_rootsOfUnity (R : Type u_4) (k : ℕ) [NeZero k] [CommRing R] [IsDomain R] : Fintype.card ↥(rootsOfUnity k R) ≤ k

theorem map_rootsOfUnity_eq_pow_self {R : Type u_4} {F : Type u_6} {k : ℕ} [NeZero k] [CommRing R] [IsDomain R] [FunLike F R R] [RingHomClass F R R] (σ : F) (ζ : ↥(rootsOfUnity k R)) : ∃ (m : ℕ), σ ↑↑ζ = ↑↑ζ ^ m

theorem mem_rootsOfUnity_prime_pow_mul_iff (R : Type u_4) [CommRing R] [IsReduced R] (p : ℕ) (k : ℕ) (m : ℕ) [ExpChar R p] {ζ : Rˣ} : ζ ∈ rootsOfUnity (p ^ k * m) R ↔ ζ ∈ rootsOfUnity m R

@[simp]

theorem mem_rootsOfUnity_prime_pow_mul_iff' (R : Type u_4) [CommRing R] [IsReduced R] (p : ℕ) (k : ℕ) (m : ℕ) [ExpChar R p] {ζ : Rˣ} : ζ ^ (p ^ k * m) = 1 ↔ ζ ∈ rootsOfUnity m R

A variant of mem_rootsOfUnity_prime_pow_mul_iff in terms of ζ ^ _.

structure IsPrimitiveRoot {M : Type u_1} [CommMonoid M] (ζ : M) (k : ℕ) : Prop

An element ζ is a primitive k-th root of unity if ζ ^ k = 1, and if l satisfies ζ ^ l = 1 then k ∣ l.

• pow_eq_one : ζ ^ k = 1
• dvd_of_pow_eq_one : ∀ (l : ℕ), ζ ^ l = 1 → k ∣ l

theorem IsPrimitiveRoot.iff_def {M : Type u_1} [CommMonoid M] (ζ : M) (k : ℕ) : IsPrimitiveRoot ζ k ↔ ζ ^ k = 1 ∧ ∀ (l : ℕ), ζ ^ l = 1 → k ∣ l

theorem IsPrimitiveRoot.pow_eq_one {M : Type u_1} [CommMonoid M] {ζ : M} {k : ℕ} (self : IsPrimitiveRoot ζ k) : ζ ^ k = 1

theorem IsPrimitiveRoot.dvd_of_pow_eq_one {M : Type u_1} [CommMonoid M] {ζ : M} {k : ℕ} (self : IsPrimitiveRoot ζ k) (l : ℕ) : ζ ^ l = 1 → k ∣ l

def IsPrimitiveRoot.toRootsOfUnity {M : Type u_1} [CommMonoid M] {μ : M} {n : ℕ} [NeZero n] (h : IsPrimitiveRoot μ n) : ↥(rootsOfUnity n M)

Turn a primitive root μ into a member of the rootsOfUnity subgroup.

Equations

• h.toRootsOfUnity = rootsOfUnity.mkOfPowEq μ ⋯

@[simp]

theorem IsPrimitiveRoot.val_inv_toRootsOfUnity_coe {M : Type u_1} [CommMonoid M] {μ : M} {n : ℕ} [NeZero n] (h : IsPrimitiveRoot μ n) : ↑(↑h.toRootsOfUnity)⁻¹ = μ ^ (n - 1)

@[simp]

theorem IsPrimitiveRoot.val_toRootsOfUnity_coe {M : Type u_1} [CommMonoid M] {μ : M} {n : ℕ} [NeZero n] (h : IsPrimitiveRoot μ n) : ↑↑h.toRootsOfUnity = μ

def primitiveRoots (k : ℕ) (R : Type u_7) [CommRing R] [IsDomain R] : Finset R

primitiveRoots k R is the finset of primitive k-th roots of unity in the integral domain R.

Equations

• primitiveRoots k R = Finset.filter (fun (ζ : R) => IsPrimitiveRoot ζ k) (Polynomial.nthRoots k 1).toFinset

@[simp]

theorem mem_primitiveRoots {R : Type u_4} {k : ℕ} [CommRing R] [IsDomain R] {ζ : R} (h0 : 0 < k) : ζ ∈ primitiveRoots k R ↔ IsPrimitiveRoot ζ k

@[simp]

theorem primitiveRoots_zero {R : Type u_4} [CommRing R] [IsDomain R] : primitiveRoots 0 R = ∅

theorem isPrimitiveRoot_of_mem_primitiveRoots {R : Type u_4} {k : ℕ} [CommRing R] [IsDomain R] {ζ : R} (h : ζ ∈ primitiveRoots k R) : IsPrimitiveRoot ζ k

theorem IsPrimitiveRoot.mk_of_lt {M : Type u_1} [CommMonoid M] {k : ℕ} (ζ : M) (hk : 0 < k) (h1 : ζ ^ k = 1) (h : ∀ (l : ℕ), 0 < l → l < k → ζ ^ l ≠ 1) : IsPrimitiveRoot ζ k

theorem IsPrimitiveRoot.of_subsingleton {M : Type u_1} [CommMonoid M] [Subsingleton M] (x : M) : IsPrimitiveRoot x 1

theorem IsPrimitiveRoot.pow_eq_one_iff_dvd {M : Type u_1} [CommMonoid M] {k : ℕ} {ζ : M} (h : IsPrimitiveRoot ζ k) (l : ℕ) : ζ ^ l = 1 ↔ k ∣ l

theorem IsPrimitiveRoot.isUnit {M : Type u_1} [CommMonoid M] {k : ℕ} {ζ : M} (h : IsPrimitiveRoot ζ k) (h0 : 0 < k) : IsUnit ζ

theorem IsPrimitiveRoot.pow_ne_one_of_pos_of_lt {M : Type u_1} [CommMonoid M] {k : ℕ} {l : ℕ} {ζ : M} (h : IsPrimitiveRoot ζ k) (h0 : 0 < l) (hl : l < k) : ζ ^ l ≠ 1

theorem IsPrimitiveRoot.ne_one {M : Type u_1} [CommMonoid M] {k : ℕ} {ζ : M} (h : IsPrimitiveRoot ζ k) (hk : 1 < k) : ζ ≠ 1

theorem IsPrimitiveRoot.pow_inj {M : Type u_1} [CommMonoid M] {k : ℕ} {ζ : M} (h : IsPrimitiveRoot ζ k) ⦃i : ℕ⦄ ⦃j : ℕ⦄ (hi : i < k) (hj : j < k) (H : ζ ^ i = ζ ^ j) : i = j

theorem IsPrimitiveRoot.one {M : Type u_1} [CommMonoid M] : IsPrimitiveRoot 1 1

@[simp]

theorem IsPrimitiveRoot.one_right_iff {M : Type u_1} [CommMonoid M] {ζ : M} : IsPrimitiveRoot ζ 1 ↔ ζ = 1

@[simp]

theorem IsPrimitiveRoot.coe_submonoidClass_iff {k : ℕ} {M : Type u_7} {B : Type u_8} [CommMonoid M] [SetLike B M] [SubmonoidClass B M] {N : B} {ζ : ↥N} : IsPrimitiveRoot (↑ζ) k ↔ IsPrimitiveRoot ζ k

@[simp]

theorem IsPrimitiveRoot.coe_units_iff {M : Type u_1} [CommMonoid M] {k : ℕ} {ζ : Mˣ} : IsPrimitiveRoot (↑ζ) k ↔ IsPrimitiveRoot ζ k

theorem IsPrimitiveRoot.isUnit_unit {M : Type u_1} [CommMonoid M] {ζ : M} {n : ℕ} (hn : 0 < n) (hζ : IsPrimitiveRoot ζ n) : IsPrimitiveRoot ⋯.unit n

theorem IsPrimitiveRoot.isUnit_unit' {G : Type u_3} [DivisionCommMonoid G] {ζ : G} {n : ℕ} (hn : 0 < n) (hζ : IsPrimitiveRoot ζ n) : IsPrimitiveRoot ⋯.unit' n

theorem IsPrimitiveRoot.pow_of_coprime {M : Type u_1} [CommMonoid M] {k : ℕ} {ζ : M} (h : IsPrimitiveRoot ζ k) (i : ℕ) (hi : i.Coprime k) : IsPrimitiveRoot (ζ ^ i) k

theorem IsPrimitiveRoot.pow_of_prime {M : Type u_1} [CommMonoid M] {k : ℕ} {ζ : M} (h : IsPrimitiveRoot ζ k) {p : ℕ} (hprime : Nat.Prime p) (hdiv : ¬p ∣ k) : IsPrimitiveRoot (ζ ^ p) k

theorem IsPrimitiveRoot.pow_iff_coprime {M : Type u_1} [CommMonoid M] {k : ℕ} {ζ : M} (h : IsPrimitiveRoot ζ k) (h0 : 0 < k) (i : ℕ) : IsPrimitiveRoot (ζ ^ i) k ↔ i.Coprime k

theorem IsPrimitiveRoot.orderOf {M : Type u_1} [CommMonoid M] (ζ : M) : IsPrimitiveRoot ζ (orderOf ζ)

theorem IsPrimitiveRoot.unique {M : Type u_1} [CommMonoid M] {k : ℕ} {l : ℕ} {ζ : M} (hk : IsPrimitiveRoot ζ k) (hl : IsPrimitiveRoot ζ l) : k = l

theorem IsPrimitiveRoot.eq_orderOf {M : Type u_1} [CommMonoid M] {k : ℕ} {ζ : M} (h : IsPrimitiveRoot ζ k) : k = orderOf ζ

theorem IsPrimitiveRoot.iff {M : Type u_1} [CommMonoid M] {k : ℕ} {ζ : M} (hk : 0 < k) : IsPrimitiveRoot ζ k ↔ ζ ^ k = 1 ∧ ∀ (l : ℕ), 0 < l → l < k → ζ ^ l ≠ 1

theorem IsPrimitiveRoot.not_iff {M : Type u_1} [CommMonoid M] {k : ℕ} {ζ : M} : ¬IsPrimitiveRoot ζ k ↔ orderOf ζ ≠ k

theorem IsPrimitiveRoot.pow_mul_pow_lcm {M : Type u_1} [CommMonoid M] {k : ℕ} {ζ : M} {ζ' : M} {k' : ℕ} (hζ : IsPrimitiveRoot ζ k) (hζ' : IsPrimitiveRoot ζ' k') (hk : k ≠ 0) (hk' : k' ≠ 0) : IsPrimitiveRoot (ζ ^ (k / k.factorizationLCMLeft k') * ζ' ^ (k' / k.factorizationLCMRight k')) (k.lcm k')

theorem IsPrimitiveRoot.pow_of_dvd {M : Type u_1} [CommMonoid M] {k : ℕ} {ζ : M} (h : IsPrimitiveRoot ζ k) {p : ℕ} (hp : p ≠ 0) (hdiv : p ∣ k) : IsPrimitiveRoot (ζ ^ p) (k / p)

theorem IsPrimitiveRoot.mem_rootsOfUnity {M : Type u_1} [CommMonoid M] {ζ : Mˣ} {n : ℕ} (h : IsPrimitiveRoot ζ n) : ζ ∈ rootsOfUnity n M

theorem IsPrimitiveRoot.pow {M : Type u_1} [CommMonoid M] {ζ : M} {n : ℕ} {a : ℕ} {b : ℕ} (hn : 0 < n) (h : IsPrimitiveRoot ζ n) (hprod : n = a * b) : IsPrimitiveRoot (ζ ^ a) b

If there is an n-th primitive root of unity in R and b divides n, then there is a b-th primitive root of unity in R.

theorem IsPrimitiveRoot.injOn_pow {M : Type u_1} [CommMonoid M] {n : ℕ} {ζ : M} (hζ : IsPrimitiveRoot ζ n) : Set.InjOn (fun (x : ℕ) => ζ ^ x) ↑(Finset.range n)

theorem IsPrimitiveRoot.map_of_injective {M : Type u_1} {N : Type u_2} {F : Type u_6} [CommMonoid M] [CommMonoid N] {k : ℕ} {ζ : M} {f : F} [FunLike F M N] [MonoidHomClass F M N] (h : IsPrimitiveRoot ζ k) (hf : Function.Injective ⇑f) : IsPrimitiveRoot (f ζ) k

theorem IsPrimitiveRoot.of_map_of_injective {M : Type u_1} {N : Type u_2} {F : Type u_6} [CommMonoid M] [CommMonoid N] {k : ℕ} {ζ : M} {f : F} [FunLike F M N] [MonoidHomClass F M N] (h : IsPrimitiveRoot (f ζ) k) (hf : Function.Injective ⇑f) : IsPrimitiveRoot ζ k

theorem IsPrimitiveRoot.map_iff_of_injective {M : Type u_1} {N : Type u_2} {F : Type u_6} [CommMonoid M] [CommMonoid N] {k : ℕ} {ζ : M} {f : F} [FunLike F M N] [MonoidHomClass F M N] (hf : Function.Injective ⇑f) : IsPrimitiveRoot (f ζ) k ↔ IsPrimitiveRoot ζ k

theorem IsPrimitiveRoot.zero {M₀ : Type u_7} [CommMonoidWithZero M₀] [Nontrivial M₀] : IsPrimitiveRoot 0 0

theorem IsPrimitiveRoot.ne_zero {k : ℕ} {M₀ : Type u_7} [CommMonoidWithZero M₀] [Nontrivial M₀] {ζ : M₀} (h : IsPrimitiveRoot ζ k) : k ≠ 0 → ζ ≠ 0

theorem IsPrimitiveRoot.injOn_pow_mul {M₀ : Type u_7} [CancelCommMonoidWithZero M₀] {n : ℕ} {ζ : M₀} (hζ : IsPrimitiveRoot ζ n) {α : M₀} (hα : α ≠ 0) : Set.InjOn (fun (x : ℕ) => ζ ^ x * α) ↑(Finset.range n)

theorem IsPrimitiveRoot.zpow_eq_one {G : Type u_3} [DivisionCommMonoid G] {k : ℕ} {ζ : G} (h : IsPrimitiveRoot ζ k) : ζ ^ ↑k = 1

theorem IsPrimitiveRoot.zpow_eq_one_iff_dvd {G : Type u_3} [DivisionCommMonoid G] {k : ℕ} {ζ : G} (h : IsPrimitiveRoot ζ k) (l : ℤ) : ζ ^ l = 1 ↔ ↑k ∣ l

theorem IsPrimitiveRoot.inv {G : Type u_3} [DivisionCommMonoid G] {k : ℕ} {ζ : G} (h : IsPrimitiveRoot ζ k) : IsPrimitiveRoot ζ⁻¹ k

@[simp]

theorem IsPrimitiveRoot.inv_iff {G : Type u_3} [DivisionCommMonoid G] {k : ℕ} {ζ : G} : IsPrimitiveRoot ζ⁻¹ k ↔ IsPrimitiveRoot ζ k

theorem IsPrimitiveRoot.zpow_of_gcd_eq_one {G : Type u_3} [DivisionCommMonoid G] {k : ℕ} {ζ : G} (h : IsPrimitiveRoot ζ k) (i : ℤ) (hi : i.gcd ↑k = 1) : IsPrimitiveRoot (ζ ^ i) k

theorem IsPrimitiveRoot.sub_one_ne_zero {R : Type u_4} [CommRing R] {n : ℕ} {ζ : R} (hn : 1 < n) (hζ : IsPrimitiveRoot ζ n) : ζ - 1 ≠ 0

@[simp]

theorem IsPrimitiveRoot.primitiveRoots_one {R : Type u_4} [CommRing R] [IsDomain R] : primitiveRoots 1 R = {1}

theorem IsPrimitiveRoot.neZero' {R : Type u_4} {ζ : R} [CommRing R] [IsDomain R] {n : ℕ} [NeZero n] (hζ : IsPrimitiveRoot ζ n) : NeZero ↑n

theorem IsPrimitiveRoot.mem_nthRootsFinset {R : Type u_4} {k : ℕ} {ζ : R} [CommRing R] [IsDomain R] (hζ : IsPrimitiveRoot ζ k) (hk : 0 < k) : ζ ∈ Polynomial.nthRootsFinset k R

theorem IsPrimitiveRoot.eq_neg_one_of_two_right {R : Type u_4} [CommRing R] [NoZeroDivisors R] {ζ : R} (h : IsPrimitiveRoot ζ 2) : ζ = -1

theorem IsPrimitiveRoot.neg_one {R : Type u_4} [CommRing R] (p : ℕ) [Nontrivial R] [h : CharP R p] (hp : p ≠ 2) : IsPrimitiveRoot (-1) 2

theorem IsPrimitiveRoot.geom_sum_eq_zero {R : Type u_4} {k : ℕ} [CommRing R] [IsDomain R] {ζ : R} (hζ : IsPrimitiveRoot ζ k) (hk : 1 < k) : ∑ i ∈ Finset.range k, ζ ^ i = 0

If 1 < k then (∑ i ∈ range k, ζ ^ i) = 0.

theorem IsPrimitiveRoot.pow_sub_one_eq {R : Type u_4} {k : ℕ} [CommRing R] [IsDomain R] {ζ : R} (hζ : IsPrimitiveRoot ζ k) (hk : 1 < k) : ζ ^ k.pred = -∑ i ∈ Finset.range k.pred, ζ ^ i

If 1 < k, then ζ ^ k.pred = -(∑ i ∈ range k.pred, ζ ^ i).

def IsPrimitiveRoot.zmodEquivZPowers {R : Type u_4} {k : ℕ} [CommRing R] {ζ : Rˣ} (h : IsPrimitiveRoot ζ k) : ZMod k ≃+ Additive ↥(Subgroup.zpowers ζ)

The (additive) monoid equivalence between ZMod k and the powers of a primitive root of unity ζ.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem IsPrimitiveRoot.zmodEquivZPowers_apply_coe_int {R : Type u_4} {k : ℕ} [CommRing R] {ζ : Rˣ} (h : IsPrimitiveRoot ζ k) (i : ℤ) : h.zmodEquivZPowers ↑i = Additive.ofMul ⟨ζ ^ i, ⋯⟩

@[simp]

theorem IsPrimitiveRoot.zmodEquivZPowers_apply_coe_nat {R : Type u_4} {k : ℕ} [CommRing R] {ζ : Rˣ} (h : IsPrimitiveRoot ζ k) (i : ℕ) : h.zmodEquivZPowers ↑i = Additive.ofMul ⟨ζ ^ i, ⋯⟩

@[simp]

theorem IsPrimitiveRoot.zmodEquivZPowers_symm_apply_zpow {R : Type u_4} {k : ℕ} [CommRing R] {ζ : Rˣ} (h : IsPrimitiveRoot ζ k) (i : ℤ) : h.zmodEquivZPowers.symm (Additive.ofMul ⟨ζ ^ i, ⋯⟩) = ↑i

@[simp]

theorem IsPrimitiveRoot.zmodEquivZPowers_symm_apply_zpow' {R : Type u_4} {k : ℕ} [CommRing R] {ζ : Rˣ} (h : IsPrimitiveRoot ζ k) (i : ℤ) : h.zmodEquivZPowers.symm ⟨ζ ^ i, ⋯⟩ = ↑i

@[simp]

theorem IsPrimitiveRoot.zmodEquivZPowers_symm_apply_pow {R : Type u_4} {k : ℕ} [CommRing R] {ζ : Rˣ} (h : IsPrimitiveRoot ζ k) (i : ℕ) : h.zmodEquivZPowers.symm (Additive.ofMul ⟨ζ ^ i, ⋯⟩) = ↑i

@[simp]

theorem IsPrimitiveRoot.zmodEquivZPowers_symm_apply_pow' {R : Type u_4} {k : ℕ} [CommRing R] {ζ : Rˣ} (h : IsPrimitiveRoot ζ k) (i : ℕ) : h.zmodEquivZPowers.symm ⟨ζ ^ i, ⋯⟩ = ↑i

theorem IsPrimitiveRoot.zpowers_eq {R : Type u_4} [CommRing R] [IsDomain R] {k : ℕ} [NeZero k] {ζ : Rˣ} (h : IsPrimitiveRoot ζ k) : Subgroup.zpowers ζ = rootsOfUnity k R

theorem IsPrimitiveRoot.map_rootsOfUnity {R : Type u_4} [CommRing R] [IsDomain R] {S : Type u_7} {F : Type u_8} [CommRing S] [IsDomain S] [FunLike F R S] [MonoidHomClass F R S] {ζ : R} {n : ℕ} [NeZero n] (hζ : IsPrimitiveRoot ζ n) {f : F} (hf : Function.Injective ⇑f) : Subgroup.map (Units.map ↑f) (rootsOfUnity n R) = rootsOfUnity n S

noncomputable def rootsOfUnityEquivOfPrimitiveRoots {R : Type u_4} [CommRing R] [IsDomain R] {S : Type u_7} {F : Type u_8} [CommRing S] [IsDomain S] [FunLike F R S] [MonoidHomClass F R S] {n : ℕ} [NeZero n] {f : F} (hf : Function.Injective ⇑f) (hζ : (primitiveRoots n R).Nonempty) : ↥(rootsOfUnity n R) ≃* ↥(rootsOfUnity n S)

If R contains an n-th primitive root, and S/R is a ring extension, then the n-th roots of unity in R and S are isomorphic. Also see IsPrimitiveRoot.map_rootsOfUnity for the equality as Subgroup Sˣ.

Equations

• rootsOfUnityEquivOfPrimitiveRoots hf hζ = ((rootsOfUnity n R).equivMapOfInjective (Units.map ↑f) ⋯).trans (MulEquiv.subgroupCongr ⋯)

theorem val_rootsOfUnityEquivOfPrimitiveRoots_apply_coe {R : Type u_4} [CommRing R] [IsDomain R] {S : Type u_7} {F : Type u_8} [CommRing S] [IsDomain S] [FunLike F R S] [MonoidHomClass F R S] {n : ℕ} [NeZero n] {f : F} (hf : Function.Injective ⇑f) (hζ : (primitiveRoots n R).Nonempty) : ∀ (a : ↥(rootsOfUnity n R)), ↑↑((rootsOfUnityEquivOfPrimitiveRoots hf hζ) a) = f ↑↑a

theorem rootsOfUnityEquivOfPrimitiveRoots_apply_coe_inv_val {R : Type u_4} [CommRing R] [IsDomain R] {S : Type u_7} {F : Type u_8} [CommRing S] [IsDomain S] [FunLike F R S] [MonoidHomClass F R S] {n : ℕ} [NeZero n] {f : F} (hf : Function.Injective ⇑f) (hζ : (primitiveRoots n R).Nonempty) : ∀ (a : ↥(rootsOfUnity n R)), ⋯ = ⋯

theorem rootsOfUnityEquivOfPrimitiveRoots_symm_apply {R : Type u_4} [CommRing R] [IsDomain R] {S : Type u_7} {F : Type u_8} [CommRing S] [IsDomain S] [FunLike F R S] [MonoidHomClass F R S] {n : ℕ} [NeZero n] {f : F} (hf : Function.Injective ⇑f) (hζ : (primitiveRoots n R).Nonempty) (η : ↥(rootsOfUnity n S)) : f ↑↑((rootsOfUnityEquivOfPrimitiveRoots hf hζ).symm η) = ↑↑η

theorem IsPrimitiveRoot.eq_pow_of_mem_rootsOfUnity {R : Type u_4} [CommRing R] [IsDomain R] {k : ℕ} [NeZero k] {ζ : Rˣ} {ξ : Rˣ} (h : IsPrimitiveRoot ζ k) (hξ : ξ ∈ rootsOfUnity k R) : ∃ i < k, ζ ^ i = ξ

theorem IsPrimitiveRoot.eq_pow_of_pow_eq_one {R : Type u_4} [CommRing R] [IsDomain R] {k : ℕ} [NeZero k] {ζ : R} {ξ : R} (h : IsPrimitiveRoot ζ k) (hξ : ξ ^ k = 1) : ∃ i < k, ζ ^ i = ξ

theorem IsPrimitiveRoot.isPrimitiveRoot_iff' {R : Type u_4} [CommRing R] [IsDomain R] {k : ℕ} [NeZero k] {ζ : Rˣ} {ξ : Rˣ} (h : IsPrimitiveRoot ζ k) : IsPrimitiveRoot ξ k ↔ ∃ i < k, i.Coprime k ∧ ζ ^ i = ξ

theorem IsPrimitiveRoot.isPrimitiveRoot_iff {R : Type u_4} [CommRing R] [IsDomain R] {k : ℕ} [NeZero k] {ζ : R} {ξ : R} (h : IsPrimitiveRoot ζ k) : IsPrimitiveRoot ξ k ↔ ∃ i < k, i.Coprime k ∧ ζ ^ i = ξ

theorem IsPrimitiveRoot.nthRoots_eq {R : Type u_4} [CommRing R] [IsDomain R] {n : ℕ} {ζ : R} (hζ : IsPrimitiveRoot ζ n) {α : R} {a : R} (e : α ^ n = a) : Polynomial.nthRoots n a = Multiset.map (fun (x : ℕ) => ζ ^ x * α) (Multiset.range n)

theorem IsPrimitiveRoot.card_nthRoots {R : Type u_4} [CommRing R] [IsDomain R] {n : ℕ} {ζ : R} (hζ : IsPrimitiveRoot ζ n) (a : R) : Multiset.card (Polynomial.nthRoots n a) = if ∃ (α : R), α ^ n = a then n else 0

theorem IsPrimitiveRoot.card_rootsOfUnity' {R : Type u_4} [CommRing R] {ζ : Rˣ} [IsDomain R] {n : ℕ} [NeZero n] (h : IsPrimitiveRoot ζ n) : Fintype.card ↥(rootsOfUnity n R) = n

A variant of IsPrimitiveRoot.card_rootsOfUnity for ζ : Rˣ.

theorem IsPrimitiveRoot.card_rootsOfUnity {R : Type u_4} [CommRing R] [IsDomain R] {ζ : R} {n : ℕ} [NeZero n] (h : IsPrimitiveRoot ζ n) : Fintype.card ↥(rootsOfUnity n R) = n

theorem IsPrimitiveRoot.card_nthRoots_one {R : Type u_4} [CommRing R] [IsDomain R] {ζ : R} {n : ℕ} (h : IsPrimitiveRoot ζ n) : Multiset.card (Polynomial.nthRoots n 1) = n

The cardinality of the multiset nthRoots ↑n (1 : R) is n if there is a primitive root of unity in R.

theorem IsPrimitiveRoot.nthRoots_nodup {R : Type u_4} [CommRing R] [IsDomain R] {ζ : R} {n : ℕ} (h : IsPrimitiveRoot ζ n) {a : R} (ha : a ≠ 0) : (Polynomial.nthRoots n a).Nodup

theorem IsPrimitiveRoot.nthRoots_one_nodup {R : Type u_4} [CommRing R] [IsDomain R] {ζ : R} {n : ℕ} (h : IsPrimitiveRoot ζ n) : (Polynomial.nthRoots n 1).Nodup

The multiset nthRoots ↑n (1 : R) has no repeated elements if there is a primitive root of unity in R.

@[simp]

theorem IsPrimitiveRoot.card_nthRootsFinset {R : Type u_4} [CommRing R] [IsDomain R] {ζ : R} {n : ℕ} (h : IsPrimitiveRoot ζ n) : (Polynomial.nthRootsFinset n R).card = n

theorem IsPrimitiveRoot.card_primitiveRoots {R : Type u_4} [CommRing R] [IsDomain R] {ζ : R} {k : ℕ} (h : IsPrimitiveRoot ζ k) : (primitiveRoots k R).card = k.totient

If an integral domain has a primitive k-th root of unity, then it has φ k of them.

theorem IsPrimitiveRoot.disjoint {R : Type u_4} [CommRing R] [IsDomain R] {k : ℕ} {l : ℕ} (h : k ≠ l) : Disjoint (primitiveRoots k R) (primitiveRoots l R)

The sets primitiveRoots k R are pairwise disjoint.

theorem IsPrimitiveRoot.nthRoots_one_eq_biUnion_primitiveRoots {R : Type u_4} [CommRing R] [IsDomain R] {ζ : R} {n : ℕ} (h : IsPrimitiveRoot ζ n) : Polynomial.nthRootsFinset n R = n.divisors.biUnion fun (i : ℕ) => primitiveRoots i R

nthRoots n as a Finset is equal to the union of primitiveRoots i R for i ∣ n if there is a primitive nth root of unity in R.

noncomputable def IsPrimitiveRoot.autToPow (R : Type u_4) {S : Type u_5} [CommRing S] [IsDomain S] {μ : S} {n : ℕ} (hμ : IsPrimitiveRoot μ n) [CommRing R] [Algebra R S] [NeZero n] : (S ≃ₐ[R] S) →* (ZMod n)ˣ

The MonoidHom that takes an automorphism to the power of μ that μ gets mapped to under it.

Equations

• IsPrimitiveRoot.autToPow R hμ = { toFun := fun (σ : S ≃ₐ[R] S) => ↑⋯.choose, map_one' := ⋯, map_mul' := ⋯ }.toHomUnits

theorem IsPrimitiveRoot.coe_autToPow_apply (R : Type u_4) {S : Type u_5} [CommRing S] [IsDomain S] {μ : S} {n : ℕ} (hμ : IsPrimitiveRoot μ n) [CommRing R] [Algebra R S] [NeZero n] (f : S ≃ₐ[R] S) : ↑((IsPrimitiveRoot.autToPow R hμ) f) = ↑⋯.choose

@[simp]

theorem IsPrimitiveRoot.autToPow_spec (R : Type u_4) {S : Type u_5} [CommRing S] [IsDomain S] {μ : S} {n : ℕ} (hμ : IsPrimitiveRoot μ n) [CommRing R] [Algebra R S] [NeZero n] (f : S ≃ₐ[R] S) : μ ^ (↑((IsPrimitiveRoot.autToPow R hμ) f)).val = f μ