Primitive roots of unity

We define a predicate IsPrimitiveRoot on commutative monoids, expressing that an element is a primitive root of unity.

Main definitions

• 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

• 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

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 with how rootsOfUnity is implemented (as a subgroup of the Units), but lemmas like IsPrimitiveRoot.isUnit and IsPrimitiveRoot.coe_units_iff should provide the necessary glue.

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

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_toRootsOfUnity_coe {M : Type u_1} [CommMonoid M] {μ : M} {n : ℕ} [NeZero n] (h : IsPrimitiveRoot μ n) : ↑↑h.toRootsOfUnity = μ

@[simp]

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

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 = {ζ ∈ (Polynomial.nthRoots k 1).toFinset | IsPrimitiveRoot ζ k}

@[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} {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.exists_pos {M : Type u_1} [CommMonoid M] {ζ : M} {k : ℕ} (hζ : ζ ^ k = 1) (hk : k ≠ 0) : ∃ k' > 0, IsPrimitiveRoot ζ k'

theorem IsPrimitiveRoot.existsUnique {M : Type u_1} [CommMonoid M] {ζ : M} : ∃! k : ℕ, IsPrimitiveRoot ζ k

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 1

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ˣ} (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} (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ˣ} (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} (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) {α 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) : (Polynomial.nthRoots n a).card = 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) : (Polynomial.nthRoots n 1).card = 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 1).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] [DecidableEq R] {n : ℕ} : Polynomial.nthRootsFinset n 1 = 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.

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) : ↑((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) : μ ^ (↑((autToPow R hμ) f)).val = f μ

theorem IsCyclic.exists_apply_ne_one {G : Type u_7} {G' : Type u_8} [Group G] [IsCyclic G] [Finite G] [CommGroup G'] (hG' : ∃ (ζ : G'), IsPrimitiveRoot ζ (Nat.card G)) ⦃a : G⦄ (ha : a ≠ 1) : ∃ (φ : G →* G'), φ a ≠ 1

If G is cyclic of order n and G' contains a primitive nth root of unity, then for each a : G with a ≠ 1 there is a homomorphism φ : G →* G' such that φ a ≠ 1.

theorem ZMod.exists_monoidHom_apply_ne_one {M : Type u_7} [CommMonoid M] {n : ℕ} [NeZero n] (hG : ∃ (ζ : M), IsPrimitiveRoot ζ n) {a : ZMod n} (ha : a ≠ 0) : ∃ (φ : Multiplicative (ZMod n) →* Mˣ), φ (Multiplicative.ofAdd a) ≠ 1

If M is a commutative group that contains a primitive nth root of unity and a : ZMod n is nonzero, then there exists a group homomorphism φ from the additive group ZMod n to the multiplicative group Mˣ such that φ a ≠ 1.