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 : ℕ+, instead of n : ℕ, because almost all lemmas need the positivity assumption, and in particular the type class instances for Fintype and IsCyclic.

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 = { toSubmonoid := { toSubsemigroup := { 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

@[simp]

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

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

@[simp]

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

def rootsOfUnity.mkOfPowEq {M : Type u_1} [CommMonoid M] (ζ : M) {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 = { val := Units.ofPowEqOne ζ (↑n) h ⋯, property := ⋯ }

@[simp]

theorem rootsOfUnity.coe_mkOfPowEq {M : Type u_1} [CommMonoid M] {ζ : M} {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

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

@[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

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

@[simp]

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

@[simp]

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

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

def rootsOfUnityEquivNthRoots (R : Type u_4) (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 : ℕ+} [CommRing R] [IsDomain R] (x : ↥(rootsOfUnity k R)) : ↑((rootsOfUnityEquivNthRoots R k) x) = ↑↑x

@[simp]

theorem rootsOfUnityEquivNthRoots_symm_apply {R : Type u_4} {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 : ℕ+) [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 : ℕ+) [CommRing R] [IsDomain R] : IsCyclic ↥(rootsOfUnity k R)

Equations

• ⋯ = ⋯

theorem card_rootsOfUnity (R : Type u_4) (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 : ℕ+} [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 ({ val := p, property := ⋯ } ^ 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

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

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

@[simp]

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

@[simp]

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

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

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

Equations

• IsPrimitiveRoot.toRootsOfUnity h = rootsOfUnity.mkOfPowEq μ ⋯

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) (Multiset.toFinset (Polynomial.nthRoots k 1))

@[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 (IsUnit.unit ⋯) n

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

theorem IsPrimitiveRoot.pow_of_coprime {M : Type u_1} [CommMonoid M] {k : ℕ} {ζ : M} (h : IsPrimitiveRoot ζ k) (i : ℕ) (hi : Nat.Coprime i 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 ↔ Nat.Coprime i 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_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 : Int.gcd i ↑k = 1) : IsPrimitiveRoot (ζ ^ i) k

theorem IsPrimitiveRoot.sub_one_ne_zero {R : Type u_4} [CommRing R] {n : ℕ} (hn : 1 < n) {ζ : R} (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 : ℕ+} (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) : (Finset.sum (Finset.range k) fun (i : ℕ) => ζ ^ i) = 0

If 1 < k then (∑ i in 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) : ζ ^ Nat.pred k = -Finset.sum (Finset.range (Nat.pred k)) fun (i : ℕ) => ζ ^ i

If 1 < k, then ζ ^ k.pred = -(∑ i in 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 : ℤ) : (IsPrimitiveRoot.zmodEquivZPowers h) ↑i = Additive.ofMul { val := ζ ^ i, property := ⋯ }

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

theorem IsPrimitiveRoot.zpowers_eq {R : Type u_4} [CommRing R] [IsDomain R] {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 : ℕ+} (hζ : IsPrimitiveRoot ζ ↑n) {f : F} (hf : Function.Injective ⇑f) : Subgroup.map (Units.map ↑f) (rootsOfUnity n R) = rootsOfUnity n S

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 : ℕ+} {f : F} (hf : Function.Injective ⇑f) (hζ : (primitiveRoots (↑n) R).Nonempty) : ∀ (a : ↥(rootsOfUnity n R)), ⋯ = ⋯

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 : ℕ+} {f : F} (hf : Function.Injective ⇑f) (hζ : (primitiveRoots (↑n) R).Nonempty) : ∀ (a : ↥(rootsOfUnity n R)), ↑↑((rootsOfUnityEquivOfPrimitiveRoots hf hζ) a) = f ↑↑a

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 : ℕ+} {f : F} (hf : Function.Injective ⇑f) (hζ : (primitiveRoots (↑n) R).Nonempty) : ↥(rootsOfUnity n R) ≃* ↥(rootsOfUnity n S)

If R contains a 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ζ = MulEquiv.trans (Subgroup.equivMapOfInjective (rootsOfUnity n R) (Units.map ↑f) ⋯) (MulEquiv.subgroupCongr ⋯)

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 : ℕ+} {f : F} (hf : Function.Injective ⇑f) (hζ : (primitiveRoots (↑n) R).Nonempty) (η : ↥(rootsOfUnity n S)) : f ↑↑((MulEquiv.symm (rootsOfUnityEquivOfPrimitiveRoots hf hζ)) η) = ↑↑η

theorem IsPrimitiveRoot.eq_pow_of_mem_rootsOfUnity {R : Type u_4} [CommRing R] [IsDomain R] {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 : ℕ} {ζ : R} {ξ : R} (h : IsPrimitiveRoot ζ k) (hξ : ξ ^ k = 1) (h0 : 0 < k) : ∃ i < k, ζ ^ i = ξ

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

theorem IsPrimitiveRoot.isPrimitiveRoot_iff {R : Type u_4} [CommRing R] [IsDomain R] {k : ℕ} {ζ : R} {ξ : R} (h : IsPrimitiveRoot ζ k) (h0 : 0 < k) : IsPrimitiveRoot ξ k ↔ ∃ i < k, Nat.Coprime i 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 : ℕ+} (h : IsPrimitiveRoot ζ ↑n) : Fintype.card ↥(rootsOfUnity n R) = ↑n

theorem IsPrimitiveRoot.card_rootsOfUnity {R : Type u_4} [CommRing R] [IsDomain R] {ζ : R} {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) : Multiset.Nodup (Polynomial.nthRoots n a)

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

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 = Nat.totient k

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 = Finset.biUnion (Nat.divisors ↑n) 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 root of unity in R. This holds for any Nat, not just PNat, see nthRoots_one_eq_bUnion_primitive_roots.

theorem IsPrimitiveRoot.nthRoots_one_eq_biUnion_primitiveRoots {R : Type u_4} [CommRing R] [IsDomain R] {ζ : R} {n : ℕ} (h : IsPrimitiveRoot ζ n) : Polynomial.nthRootsFinset n R = Finset.biUnion (Nat.divisors n) 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 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] : (S ≃ₐ[R] S) →* (ZMod ↑n)ˣ

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

Equations

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

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] (f : S ≃ₐ[R] S) : ↑((IsPrimitiveRoot.autToPow R hμ) f) = ↑(Exists.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] (f : S ≃ₐ[R] S) : μ ^ ZMod.val ↑((IsPrimitiveRoot.autToPow R hμ) f) = f μ