mathlib3 documentation

ring_theory.roots_of_unity.basic

Roots of unity and primitive roots of unity #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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 is_primitive_root on commutative monoids, expressing that an element is a primitive root of unity.

Main definitions #

roots_of_unity n M, for n : ℕ+ is the subgroup of the units of a commutative monoid M consisting of elements x that satisfy x ^ n = 1.
is_primitive_root ζ k: an element ζ is a primitive k-th root of unity if ζ ^ k = 1, and if l satisfies ζ ^ l = 1 then k ∣ l.
primitive_roots k R: the finset of primitive k-th roots of unity in an integral domain R.
is_primitive_root.aut_to_pow: 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 #

roots_of_unity.is_cyclic: the roots of unity in an integral domain form a cyclic group.
is_primitive_root.zmod_equiv_zpowers: zmod k is equivalent to the subgroup generated by a primitive k-th root of unity.
is_primitive_root.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.
is_primitive_root.card_primitive_roots: if an integral domain has a primitive k-th root of unity, then it has φ k of them.

Implementation details #

It is desirable that roots_of_unity 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 roots_of_unity n for n : ℕ+, instead of n : ℕ, because almost all lemmas need the positivity assumption, and in particular the type class instances for fintype and is_cyclic.

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 is_primitive_root.is_unit and is_primitive_root.coe_units_iff should provide the necessary glue.

def roots_of_unity (k : ℕ+) (M : Type u_1) [comm_monoid M] :

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

Equations

roots_of_unity k M = {carrier := {ζ : Mˣ | ζ ^ ↑k = 1}, mul_mem' := _, one_mem' := _, inv_mem' := _}

Instances for ↥roots_of_unity

@[simp]

theorem mem_roots_of_unity {M : Type u_1} [comm_monoid M] (k : ℕ+) (ζ : Mˣ) :

ζ ∈ roots_of_unity k M ↔ ζ ^ ↑k = 1

theorem mem_roots_of_unity' {M : Type u_1} [comm_monoid M] (k : ℕ+) (ζ : Mˣ) :

ζ ∈ roots_of_unity k M ↔ ↑ζ ^ ↑k = 1

theorem roots_of_unity.coe_injective {M : Type u_1} [comm_monoid M] {n : ℕ+} :

function.injective coe

@[simp]

theorem roots_of_unity.coe_mk_of_pow_eq_coe {M : Type u_1} [comm_monoid M] (ζ : M) {n : ℕ+} (h : ζ ^ ↑n = 1) :

↑↑(roots_of_unity.mk_of_pow_eq ζ h) = ζ

def roots_of_unity.mk_of_pow_eq {M : Type u_1} [comm_monoid M] (ζ : M) {n : ℕ+} (h : ζ ^ ↑n = 1) :

↥(roots_of_unity n M)

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

Equations

roots_of_unity.mk_of_pow_eq ζ h = ⟨units.of_pow_eq_one ζ ↑n h _, _⟩

@[simp]

theorem roots_of_unity.coe_mk_of_pow_eq {M : Type u_1} [comm_monoid M] {ζ : M} {n : ℕ+} (h : ζ ^ ↑n = 1) :

↑(roots_of_unity.mk_of_pow_eq ζ h) = ζ

theorem roots_of_unity_le_of_dvd {M : Type u_1} [comm_monoid M] {k l : ℕ+} (h : k ∣ l) :

roots_of_unity k M ≤ roots_of_unity l M

theorem map_roots_of_unity {M : Type u_1} {N : Type u_2} [comm_monoid M] [comm_monoid N] (f : Mˣ →* Nˣ) (k : ℕ+) :

subgroup.map f (roots_of_unity k M) ≤ roots_of_unity k N

@[norm_cast]

theorem roots_of_unity.coe_pow {R : Type u_4} {k : ℕ+} [comm_monoid R] (ζ : ↥(roots_of_unity k R)) (m : ℕ) :

↑(ζ ^ m) = ↑ζ ^ m

def restrict_roots_of_unity {R : Type u_4} {S : Type u_5} {F : Type u_6} [comm_semiring R] [comm_semiring S] [ring_hom_class F R S] (σ : F) (n : ℕ+) :

↥(roots_of_unity n R) →* ↥(roots_of_unity n S)

Restrict a ring homomorphism to the nth roots of unity

Equations

restrict_roots_of_unity σ n = let h : ∀ (ξ : ↥(roots_of_unity n R)), ⇑σ ↑ξ ^ ↑n = 1 := _ in {to_fun := λ (ξ : ↥(roots_of_unity n R)), ⟨unit_of_invertible (⇑σ ↑ξ) (invertible_of_pow_eq_one (⇑σ ↑ξ) ↑n _ _), _⟩, map_one' := _, map_mul' := _}

@[simp]

theorem restrict_roots_of_unity_coe_apply {R : Type u_4} {S : Type u_5} {F : Type u_6} {k : ℕ+} [comm_semiring R] [comm_semiring S] [ring_hom_class F R S] (σ : F) (ζ : ↥(roots_of_unity k R)) :

↑(⇑(restrict_roots_of_unity σ k) ζ) = ⇑σ ↑ζ

def ring_equiv.restrict_roots_of_unity {R : Type u_4} {S : Type u_5} [comm_semiring R] [comm_semiring S] (σ : R ≃+* S) (n : ℕ+) :

↥(roots_of_unity n R) ≃* ↥(roots_of_unity n S)

Restrict a ring isomorphism to the nth roots of unity

Equations

σ.restrict_roots_of_unity n = {to_fun := ⇑(restrict_roots_of_unity σ.to_ring_hom n), inv_fun := ⇑(restrict_roots_of_unity σ.symm.to_ring_hom n), left_inv := _, right_inv := _, map_mul' := _}

@[simp]

theorem ring_equiv.restrict_roots_of_unity_coe_apply {R : Type u_4} {S : Type u_5} {k : ℕ+} [comm_semiring R] [comm_semiring S] (σ : R ≃+* S) (ζ : ↥(roots_of_unity k R)) :

↑(⇑(σ.restrict_roots_of_unity k) ζ) = ⇑σ ↑ζ

@[simp]

theorem ring_equiv.restrict_roots_of_unity_symm {R : Type u_4} {S : Type u_5} {k : ℕ+} [comm_semiring R] [comm_semiring S] (σ : R ≃+* S) :

(σ.restrict_roots_of_unity k).symm = σ.symm.restrict_roots_of_unity k

theorem mem_roots_of_unity_iff_mem_nth_roots {R : Type u_4} {k : ℕ+} [comm_ring R] [is_domain R] {ζ : Rˣ} :

ζ ∈ roots_of_unity k R ↔ ↑ζ ∈ polynomial.nth_roots ↑k 1

def roots_of_unity_equiv_nth_roots (R : Type u_4) (k : ℕ+) [comm_ring R] [is_domain R] :

↥(roots_of_unity k R) ≃ {x // x ∈ polynomial.nth_roots ↑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 roots_of_unity is a subgroup of the group of units, whereas nth_roots is a multiset.

Equations

roots_of_unity_equiv_nth_roots R k = {to_fun := λ (x : ↥(roots_of_unity k R)), ⟨↑x, _⟩, inv_fun := λ (x : {x // x ∈ polynomial.nth_roots ↑k 1}), ⟨{val := ↑x, inv := ↑x ^ (↑k - 1), val_inv := _, inv_val := _}, _⟩, left_inv := _, right_inv := _}

@[simp]

theorem roots_of_unity_equiv_nth_roots_apply {R : Type u_4} {k : ℕ+} [comm_ring R] [is_domain R] (x : ↥(roots_of_unity k R)) :

↑(⇑(roots_of_unity_equiv_nth_roots R k) x) = ↑x

@[simp]

theorem roots_of_unity_equiv_nth_roots_symm_apply {R : Type u_4} {k : ℕ+} [comm_ring R] [is_domain R] (x : {x // x ∈ polynomial.nth_roots ↑k 1}) :

↑(⇑((roots_of_unity_equiv_nth_roots R k).symm) x) = ↑x

@[protected, instance]

noncomputable def roots_of_unity.fintype (R : Type u_4) (k : ℕ+) [comm_ring R] [is_domain R] :

fintype ↥(roots_of_unity k R)

Equations

roots_of_unity.fintype R k = fintype.of_equiv {x // x ∈ polynomial.nth_roots ↑k 1} (roots_of_unity_equiv_nth_roots R k).symm

@[protected, instance]

def roots_of_unity.is_cyclic (R : Type u_4) (k : ℕ+) [comm_ring R] [is_domain R] :

is_cyclic ↥(roots_of_unity k R)

theorem card_roots_of_unity (R : Type u_4) (k : ℕ+) [comm_ring R] [is_domain R] :

fintype.card ↥(roots_of_unity k R) ≤ ↑k

theorem map_root_of_unity_eq_pow_self {R : Type u_4} {F : Type u_6} {k : ℕ+} [comm_ring R] [is_domain R] [ring_hom_class F R R] (σ : F) (ζ : ↥(roots_of_unity k R)) :

∃ (m : ℕ), ⇑σ ↑ζ = ↑ζ ^ m

@[simp]

theorem mem_roots_of_unity_prime_pow_mul_iff (R : Type u_4) [comm_ring R] [is_reduced R] (p k : ℕ) (m : ℕ+) [hp : fact (nat.prime p)] [char_p R p] {ζ : Rˣ} :

ζ ∈ roots_of_unity (⟨p, _⟩ ^ k * m) R ↔ ζ ∈ roots_of_unity m R

structure is_primitive_root {M : Type u_1} [comm_monoid M] (ζ : M) (k : ℕ) :

Prop

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

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

@[simp]

theorem is_primitive_root.coe_inv_to_roots_of_unity_coe {M : Type u_1} [comm_monoid M] {μ : M} {n : ℕ+} (h : is_primitive_root μ ↑n) :

↑(↑(h.to_roots_of_unity))⁻¹ = μ ^ (↑n - 1)

@[simp]

theorem is_primitive_root.coe_to_roots_of_unity_coe {M : Type u_1} [comm_monoid M] {μ : M} {n : ℕ+} (h : is_primitive_root μ ↑n) :

↑↑(h.to_roots_of_unity) = μ

def is_primitive_root.to_roots_of_unity {M : Type u_1} [comm_monoid M] {μ : M} {n : ℕ+} (h : is_primitive_root μ ↑n) :

↥(roots_of_unity n M)

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

Equations

h.to_roots_of_unity = roots_of_unity.mk_of_pow_eq μ _

noncomputable def primitive_roots (k : ℕ) (R : Type u_1) [comm_ring R] [is_domain R] :

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

Equations

primitive_roots k R = finset.filter (λ (ζ : R), is_primitive_root ζ k) (polynomial.nth_roots k 1).to_finset

@[simp]

theorem mem_primitive_roots {R : Type u_4} {k : ℕ} [comm_ring R] [is_domain R] {ζ : R} (h0 : 0 < k) :

ζ ∈ primitive_roots k R ↔ is_primitive_root ζ k

@[simp]

theorem primitive_roots_zero {R : Type u_4} [comm_ring R] [is_domain R] :

primitive_roots 0 R = ∅

theorem is_primitive_root_of_mem_primitive_roots {R : Type u_4} {k : ℕ} [comm_ring R] [is_domain R] {ζ : R} (h : ζ ∈ primitive_roots k R) :

is_primitive_root ζ k

theorem is_primitive_root.iff_def {M : Type u_1} [comm_monoid M] (ζ : M) (k : ℕ) :

is_primitive_root ζ k ↔ ζ ^ k = 1 ∧ ∀ (l : ℕ), ζ ^ l = 1 → k ∣ l

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

is_primitive_root ζ k

theorem is_primitive_root.of_subsingleton {M : Type u_1} [comm_monoid M] [subsingleton M] (x : M) :

is_primitive_root x 1

theorem is_primitive_root.pow_eq_one_iff_dvd {M : Type u_1} [comm_monoid M] {k : ℕ} {ζ : M} (h : is_primitive_root ζ k) (l : ℕ) :

ζ ^ l = 1 ↔ k ∣ l

theorem is_primitive_root.is_unit {M : Type u_1} [comm_monoid M] {k : ℕ} {ζ : M} (h : is_primitive_root ζ k) (h0 : 0 < k) :

theorem is_primitive_root.pow_ne_one_of_pos_of_lt {M : Type u_1} [comm_monoid M] {k l : ℕ} {ζ : M} (h : is_primitive_root ζ k) (h0 : 0 < l) (hl : l < k) :

ζ ^ l ≠ 1

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

ζ ≠ 1

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

i = j

theorem is_primitive_root.one {M : Type u_1} [comm_monoid M] :

is_primitive_root 1 1

@[simp]

theorem is_primitive_root.one_right_iff {M : Type u_1} [comm_monoid M] {ζ : M} :

is_primitive_root ζ 1 ↔ ζ = 1

@[simp]

theorem is_primitive_root.coe_submonoid_class_iff {k : ℕ} {M : Type u_1} {B : Type u_2} [comm_monoid M] [set_like B M] [submonoid_class B M] {N : B} {ζ : ↥N} :

is_primitive_root ↑ζ k ↔ is_primitive_root ζ k

@[simp]

theorem is_primitive_root.coe_units_iff {M : Type u_1} [comm_monoid M] {k : ℕ} {ζ : Mˣ} :

is_primitive_root ↑ζ k ↔ is_primitive_root ζ k

theorem is_primitive_root.pow_of_coprime {M : Type u_1} [comm_monoid M] {k : ℕ} {ζ : M} (h : is_primitive_root ζ k) (i : ℕ) (hi : i.coprime k) :

is_primitive_root (ζ ^ i) k

theorem is_primitive_root.pow_of_prime {M : Type u_1} [comm_monoid M] {k : ℕ} {ζ : M} (h : is_primitive_root ζ k) {p : ℕ} (hprime : nat.prime p) (hdiv : ¬p ∣ k) :

is_primitive_root (ζ ^ p) k

theorem is_primitive_root.pow_iff_coprime {M : Type u_1} [comm_monoid M] {k : ℕ} {ζ : M} (h : is_primitive_root ζ k) (h0 : 0 < k) (i : ℕ) :

is_primitive_root (ζ ^ i) k ↔ i.coprime k

@[protected]

theorem is_primitive_root.order_of {M : Type u_1} [comm_monoid M] (ζ : M) :

is_primitive_root ζ (order_of ζ)

theorem is_primitive_root.unique {M : Type u_1} [comm_monoid M] {k l : ℕ} {ζ : M} (hk : is_primitive_root ζ k) (hl : is_primitive_root ζ l) :

k = l

theorem is_primitive_root.eq_order_of {M : Type u_1} [comm_monoid M] {k : ℕ} {ζ : M} (h : is_primitive_root ζ k) :

k = order_of ζ

@[protected]

theorem is_primitive_root.iff {M : Type u_1} [comm_monoid M] {k : ℕ} {ζ : M} (hk : 0 < k) :

is_primitive_root ζ k ↔ ζ ^ k = 1 ∧ ∀ (l : ℕ), 0 < l → l < k → ζ ^ l ≠ 1

@[protected]

theorem is_primitive_root.not_iff {M : Type u_1} [comm_monoid M] {k : ℕ} {ζ : M} :

¬is_primitive_root ζ k ↔ order_of ζ ≠ k

theorem is_primitive_root.pow_of_dvd {M : Type u_1} [comm_monoid M] {k : ℕ} {ζ : M} (h : is_primitive_root ζ k) {p : ℕ} (hp : p ≠ 0) (hdiv : p ∣ k) :

is_primitive_root (ζ ^ p) (k / p)

@[protected]

theorem is_primitive_root.mem_roots_of_unity {M : Type u_1} [comm_monoid M] {ζ : Mˣ} {n : ℕ+} (h : is_primitive_root ζ ↑n) :

ζ ∈ roots_of_unity n M

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

is_primitive_root (ζ ^ a) b

If there is a 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 is_primitive_root.map_of_injective {M : Type u_1} {N : Type u_2} {F : Type u_6} [comm_monoid M] [comm_monoid N] {k : ℕ} {ζ : M} {f : F} [monoid_hom_class F M N] (h : is_primitive_root ζ k) (hf : function.injective ⇑f) :

is_primitive_root (⇑f ζ) k

theorem is_primitive_root.of_map_of_injective {M : Type u_1} {N : Type u_2} {F : Type u_6} [comm_monoid M] [comm_monoid N] {k : ℕ} {ζ : M} {f : F} [monoid_hom_class F M N] (h : is_primitive_root (⇑f ζ) k) (hf : function.injective ⇑f) :

is_primitive_root ζ k

theorem is_primitive_root.map_iff_of_injective {M : Type u_1} {N : Type u_2} {F : Type u_6} [comm_monoid M] [comm_monoid N] {k : ℕ} {ζ : M} {f : F} [monoid_hom_class F M N] (hf : function.injective ⇑f) :

is_primitive_root (⇑f ζ) k ↔ is_primitive_root ζ k

theorem is_primitive_root.zero {M₀ : Type u_7} [comm_monoid_with_zero M₀] [nontrivial M₀] :

is_primitive_root 0 0

@[protected]

theorem is_primitive_root.ne_zero {k : ℕ} {M₀ : Type u_7} [comm_monoid_with_zero M₀] [nontrivial M₀] {ζ : M₀} (h : is_primitive_root ζ k) :

k ≠ 0 → ζ ≠ 0

theorem is_primitive_root.zpow_eq_one {G : Type u_3} [division_comm_monoid G] {k : ℕ} {ζ : G} (h : is_primitive_root ζ k) :

ζ ^ ↑k = 1

theorem is_primitive_root.zpow_eq_one_iff_dvd {G : Type u_3} [division_comm_monoid G] {k : ℕ} {ζ : G} (h : is_primitive_root ζ k) (l : ℤ) :

ζ ^ l = 1 ↔ ↑k ∣ l

theorem is_primitive_root.inv {G : Type u_3} [division_comm_monoid G] {k : ℕ} {ζ : G} (h : is_primitive_root ζ k) :

is_primitive_root ζ⁻¹ k

@[simp]

theorem is_primitive_root.inv_iff {G : Type u_3} [division_comm_monoid G] {k : ℕ} {ζ : G} :

is_primitive_root ζ⁻¹ k ↔ is_primitive_root ζ k

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

is_primitive_root (ζ ^ i) k

@[simp]

theorem is_primitive_root.primitive_roots_one {R : Type u_4} [comm_ring R] [is_domain R] :

primitive_roots 1 R = {1}

theorem is_primitive_root.ne_zero' {R : Type u_4} {ζ : R} [comm_ring R] [is_domain R] {n : ℕ+} (hζ : is_primitive_root ζ ↑n) :

ne_zero ↑↑n

theorem is_primitive_root.mem_nth_roots_finset {R : Type u_4} {k : ℕ} {ζ : R} [comm_ring R] [is_domain R] (hζ : is_primitive_root ζ k) (hk : 0 < k) :

ζ ∈ polynomial.nth_roots_finset k R

theorem is_primitive_root.eq_neg_one_of_two_right {R : Type u_4} [comm_ring R] [no_zero_divisors R] {ζ : R} (h : is_primitive_root ζ 2) :

ζ = -1

theorem is_primitive_root.neg_one {R : Type u_4} [comm_ring R] (p : ℕ) [nontrivial R] [h : char_p R p] (hp : p ≠ 2) :

is_primitive_root (-1) 2

theorem is_primitive_root.geom_sum_eq_zero {R : Type u_4} {k : ℕ} [comm_ring R] [is_domain R] {ζ : R} (hζ : is_primitive_root ζ k) (hk : 1 < k) :

(finset.range k).sum (λ (i : ℕ), ζ ^ i) = 0

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

theorem is_primitive_root.pow_sub_one_eq {R : Type u_4} {k : ℕ} [comm_ring R] [is_domain R] {ζ : R} (hζ : is_primitive_root ζ k) (hk : 1 < k) :

ζ ^ k.pred = -(finset.range k.pred).sum (λ (i : ℕ), ζ ^ i)

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

noncomputable def is_primitive_root.zmod_equiv_zpowers {R : Type u_4} {k : ℕ} [comm_ring R] {ζ : Rˣ} (h : is_primitive_root ζ k) :

zmod k ≃+ additive ↥(subgroup.zpowers ζ)

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

Equations

h.zmod_equiv_zpowers = add_equiv.of_bijective (⇑((int.cast_add_hom (zmod k)).lift_of_right_inverse coe zmod.int_cast_right_inverse) ⟨{to_fun := λ (i : ℤ), ⇑additive.of_mul ⟨ζ ^ i, _⟩, map_zero' := _, map_add' := _}, _⟩) _

@[simp]

theorem is_primitive_root.zmod_equiv_zpowers_apply_coe_int {R : Type u_4} {k : ℕ} [comm_ring R] {ζ : Rˣ} (h : is_primitive_root ζ k) (i : ℤ) :

⇑(h.zmod_equiv_zpowers) ↑i = ⇑additive.of_mul ⟨ζ ^ i, _⟩

@[simp]

theorem is_primitive_root.zmod_equiv_zpowers_apply_coe_nat {R : Type u_4} {k : ℕ} [comm_ring R] {ζ : Rˣ} (h : is_primitive_root ζ k) (i : ℕ) :

⇑(h.zmod_equiv_zpowers) ↑i = ⇑additive.of_mul ⟨ζ ^ i, _⟩

@[simp]

theorem is_primitive_root.zmod_equiv_zpowers_symm_apply_zpow {R : Type u_4} {k : ℕ} [comm_ring R] {ζ : Rˣ} (h : is_primitive_root ζ k) (i : ℤ) :

⇑(h.zmod_equiv_zpowers.symm) (⇑additive.of_mul ⟨ζ ^ i, _⟩) = ↑i

@[simp]

theorem is_primitive_root.zmod_equiv_zpowers_symm_apply_zpow' {R : Type u_4} {k : ℕ} [comm_ring R] {ζ : Rˣ} (h : is_primitive_root ζ k) (i : ℤ) :

⇑(h.zmod_equiv_zpowers.symm) ⟨ζ ^ i, _⟩ = ↑i

@[simp]

theorem is_primitive_root.zmod_equiv_zpowers_symm_apply_pow {R : Type u_4} {k : ℕ} [comm_ring R] {ζ : Rˣ} (h : is_primitive_root ζ k) (i : ℕ) :

⇑(h.zmod_equiv_zpowers.symm) (⇑additive.of_mul ⟨ζ ^ i, _⟩) = ↑i

@[simp]

theorem is_primitive_root.zmod_equiv_zpowers_symm_apply_pow' {R : Type u_4} {k : ℕ} [comm_ring R] {ζ : Rˣ} (h : is_primitive_root ζ k) (i : ℕ) :

⇑(h.zmod_equiv_zpowers.symm) ⟨ζ ^ i, _⟩ = ↑i

theorem is_primitive_root.zpowers_eq {R : Type u_4} [comm_ring R] [is_domain R] {k : ℕ+} {ζ : Rˣ} (h : is_primitive_root ζ ↑k) :

subgroup.zpowers ζ = roots_of_unity k R

theorem is_primitive_root.eq_pow_of_mem_roots_of_unity {R : Type u_4} [comm_ring R] [is_domain R] {k : ℕ+} {ζ ξ : Rˣ} (h : is_primitive_root ζ ↑k) (hξ : ξ ∈ roots_of_unity k R) :

∃ (i : ℕ) (hi : i < ↑k), ζ ^ i = ξ

theorem is_primitive_root.eq_pow_of_pow_eq_one {R : Type u_4} [comm_ring R] [is_domain R] {k : ℕ} {ζ ξ : R} (h : is_primitive_root ζ k) (hξ : ξ ^ k = 1) (h0 : 0 < k) :

∃ (i : ℕ) (H : i < k), ζ ^ i = ξ

theorem is_primitive_root.is_primitive_root_iff' {R : Type u_4} [comm_ring R] [is_domain R] {k : ℕ+} {ζ ξ : Rˣ} (h : is_primitive_root ζ ↑k) :

is_primitive_root ξ ↑k ↔ ∃ (i : ℕ) (H : i < ↑k) (hi : i.coprime ↑k), ζ ^ i = ξ

theorem is_primitive_root.is_primitive_root_iff {R : Type u_4} [comm_ring R] [is_domain R] {k : ℕ} {ζ ξ : R} (h : is_primitive_root ζ k) (h0 : 0 < k) :

is_primitive_root ξ k ↔ ∃ (i : ℕ) (H : i < k) (hi : i.coprime k), ζ ^ i = ξ

theorem is_primitive_root.card_roots_of_unity' {R : Type u_4} [comm_ring R] {ζ : Rˣ} [is_domain R] {n : ℕ+} (h : is_primitive_root ζ ↑n) :

fintype.card ↥(roots_of_unity n R) = ↑n

theorem is_primitive_root.card_roots_of_unity {R : Type u_4} [comm_ring R] [is_domain R] {ζ : R} {n : ℕ+} (h : is_primitive_root ζ ↑n) :

fintype.card ↥(roots_of_unity n R) = ↑n

theorem is_primitive_root.card_nth_roots {R : Type u_4} [comm_ring R] [is_domain R] {ζ : R} {n : ℕ} (h : is_primitive_root ζ n) :

⇑multiset.card (polynomial.nth_roots n 1) = n

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

theorem is_primitive_root.nth_roots_nodup {R : Type u_4} [comm_ring R] [is_domain R] {ζ : R} {n : ℕ} (h : is_primitive_root ζ n) :

(polynomial.nth_roots n 1).nodup

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

@[simp]

theorem is_primitive_root.card_nth_roots_finset {R : Type u_4} [comm_ring R] [is_domain R] {ζ : R} {n : ℕ} (h : is_primitive_root ζ n) :

(polynomial.nth_roots_finset n R).card = n

theorem is_primitive_root.card_primitive_roots {R : Type u_4} [comm_ring R] [is_domain R] {ζ : R} {k : ℕ} (h : is_primitive_root ζ k) :

(primitive_roots k R).card = k.totient

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

theorem is_primitive_root.disjoint {R : Type u_4} [comm_ring R] [is_domain R] {k l : ℕ} (h : k ≠ l) :

disjoint (primitive_roots k R) (primitive_roots l R)

The sets primitive_roots k R are pairwise disjoint.

theorem is_primitive_root.nth_roots_one_eq_bUnion_primitive_roots' {R : Type u_4} [comm_ring R] [is_domain R] {ζ : R} {n : ℕ+} (h : is_primitive_root ζ ↑n) :

polynomial.nth_roots_finset ↑n R = ↑n.divisors.bUnion (λ (i : ℕ), primitive_roots i R)

nth_roots n as a finset is equal to the union of primitive_roots i R for i ∣ n if there is a primitive root of unity in R. This holds for any nat, not just pnat, see nth_roots_one_eq_bUnion_primitive_roots.

theorem is_primitive_root.nth_roots_one_eq_bUnion_primitive_roots {R : Type u_4} [comm_ring R] [is_domain R] {ζ : R} {n : ℕ} (h : is_primitive_root ζ n) :

polynomial.nth_roots_finset n R = n.divisors.bUnion (λ (i : ℕ), primitive_roots i R)

nth_roots n as a finset is equal to the union of primitive_roots i R for i ∣ n if there is a primitive root of unity in R.

noncomputable def is_primitive_root.aut_to_pow (R : Type u_4) {S : Type u_5} [comm_ring S] [is_domain S] {μ : S} {n : ℕ+} (hμ : is_primitive_root μ ↑n) [comm_ring R] [algebra R S] :

(S ≃ₐ[R] S) →* (zmod ↑n)ˣ

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

Equations

is_primitive_root.aut_to_pow R hμ = let μ' : ↥(roots_of_unity n S) := hμ.to_roots_of_unity in have ho : order_of μ' = ↑n, from _, {to_fun := λ (σ : S ≃ₐ[R] S), ↑(_.some), map_one' := _, map_mul' := _}.to_hom_units

theorem is_primitive_root.coe_aut_to_pow_apply (R : Type u_4) {S : Type u_5} [comm_ring S] [is_domain S] {μ : S} {n : ℕ+} (hμ : is_primitive_root μ ↑n) [comm_ring R] [algebra R S] (f : S ≃ₐ[R] S) :

↑(⇑(is_primitive_root.aut_to_pow R hμ) f) = ↑(_.some)

@[simp]

theorem is_primitive_root.aut_to_pow_spec (R : Type u_4) {S : Type u_5} [comm_ring S] [is_domain S] {μ : S} {n : ℕ+} (hμ : is_primitive_root μ ↑n) [comm_ring R] [algebra R S] (f : S ≃ₐ[R] S) :

μ ^ ↑(⇑(is_primitive_root.aut_to_pow R hμ) f).val = ⇑f μ