# mathlibdocumentation

ring_theory.roots_of_unity

# 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 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.

## Main results #

• roots_of_unity.is_cyclic: the roots of unity in an integral domain form a cyclic group.
• is_primitive_root.zmod_equiv_gpowers: zmod k is equivalent to the subgroup generated by a primitive k-th root of unity.
• is_primitive_root.gpowers_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 : units M that satisfy m ^ k = 1

Equations
@[simp]
theorem mem_roots_of_unity {M : Type u_1} [comm_monoid M] (k : ℕ+) (ζ : units M) :
ζ ζ ^ k = 1
theorem roots_of_unity_le_of_dvd {M : Type u_1} [comm_monoid M] {k l : ℕ+} (h : k l) :
theorem map_roots_of_unity {M : Type u_1} {N : Type u_2} [comm_monoid M] [comm_monoid N] (f : →* ) (k : ℕ+) :
M)
theorem mem_roots_of_unity_iff_mem_nth_roots {R : Type u_5} {k : ℕ+} {ζ : units R} :
ζ
def roots_of_unity_equiv_nth_roots (R : Type u_5) (k : ℕ+) :
R) {x // x

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
@[simp]
theorem roots_of_unity_equiv_nth_roots_apply {R : Type u_5} {k : ℕ+} (x : R)) :
x) = x
@[simp]
theorem roots_of_unity_equiv_nth_roots_symm_apply {R : Type u_5} {k : ℕ+} (x : {x // x ) :
@[instance]
def roots_of_unity.fintype (R : Type u_5) (k : ℕ+) :
Equations
@[instance]
def roots_of_unity.is_cyclic (R : Type u_5) (k : ℕ+) :
theorem card_roots_of_unity (R : Type u_5) (k : ℕ+) :
theorem roots_of_unity.coe_pow {R : Type u_5} {k : ℕ+} (ζ : R)) (m : ) :
^ m) = ζ ^ m
def ring_hom.restrict_roots_of_unity {R : Type u_5} {S : Type u_6} (σ : R →+* S) (n : ℕ+) :
R) →* S)

Restrict a ring homomorphism between integral domains to the nth roots of unity

Equations
@[simp]
theorem ring_hom.restrict_roots_of_unity_coe_apply {R : Type u_5} {S : Type u_6} {k : ℕ+} (σ : R →+* S) (ζ : R)) :
( ζ) = σ ζ
def ring_equiv.restrict_roots_of_unity {R : Type u_5} {S : Type u_6} (σ : R ≃+* S) (n : ℕ+) :
R) ≃* S)

Restrict a ring isomorphism between integral domains to the nth roots of unity

Equations
@[simp]
theorem ring_equiv.restrict_roots_of_unity_coe_apply {R : Type u_5} {S : Type u_6} {k : ℕ+} (σ : R ≃+* S) (ζ : R)) :
( ζ) = σ ζ
@[simp]
theorem ring_equiv.restrict_roots_of_unity_symm {R : Type u_5} {S : Type u_6} {k : ℕ+} (σ : R ≃+* S) :
theorem ring_hom.map_root_of_unity_eq_pow_self {R : Type u_5} {k : ℕ+} (σ : R →+* R) (ζ : R)) :
∃ (m : ), σ ζ = ζ ^ m
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 = 1k l

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

def primitive_roots (k : ) (R : Type u_1)  :

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

Equations
@[simp]
theorem mem_primitive_roots {R : Type u_5} {k : } {ζ : R} (h0 : 0 < k) :
ζ
theorem is_primitive_root.iff_def {M : Type u_1} [comm_monoid M] (ζ : M) (k : ) :
ζ ^ k = 1 ∀ (l : ), ζ ^ l = 1k 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 < ll < kζ ^ l 1) :
theorem is_primitive_root.pow_eq_one_iff_dvd {M : Type u_1} [comm_monoid M] {k : } {ζ : M} (h : k) (l : ) :
ζ ^ l = 1 k l
theorem is_primitive_root.is_unit {M : Type u_1} [comm_monoid M] {k : } {ζ : M} (h : 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 : k) (h0 : 0 < l) (hl : l < k) :
ζ ^ l 1
theorem is_primitive_root.pow_inj {M : Type u_1} [comm_monoid M] {k : } {ζ : M} (h : 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] :
@[simp]
theorem is_primitive_root.one_right_iff {M : Type u_1} [comm_monoid M] {ζ : M} :
ζ = 1
@[simp]
theorem is_primitive_root.coe_units_iff {M : Type u_1} [comm_monoid M] {k : } {ζ : units M} :
theorem is_primitive_root.pow_of_coprime {M : Type u_1} [comm_monoid M] {k : } {ζ : M} (h : k) (i : ) (hi : i.coprime k) :
theorem is_primitive_root.pow_of_prime {M : Type u_1} [comm_monoid M] {k : } {ζ : M} (h : k) {p : } (hprime : nat.prime p) (hdiv : ¬p k) :
theorem is_primitive_root.pow_iff_coprime {M : Type u_1} [comm_monoid M] {k : } {ζ : M} (h : k) (h0 : 0 < k) (i : ) :
theorem is_primitive_root.gpow_eq_one {G : Type u_3} [comm_group G] {k : } {ζ : G} (h : k) :
ζ ^ k = 1
theorem is_primitive_root.gpow_eq_one_iff_dvd {G : Type u_3} [comm_group G] {k : } {ζ : G} (h : k) (l : ) :
ζ ^ l = 1 k l
theorem is_primitive_root.inv {G : Type u_3} [comm_group G] {k : } {ζ : G} (h : k) :
@[simp]
theorem is_primitive_root.inv_iff {G : Type u_3} [comm_group G] {k : } {ζ : G} :
theorem is_primitive_root.gpow_of_gcd_eq_one {G : Type u_3} [comm_group G] {k : } {ζ : G} (h : k) (i : ) (hi : i.gcd k = 1) :
@[simp]
theorem is_primitive_root.coe_subgroup_iff {G : Type u_3} [comm_group G] {k : } (H : subgroup G) {ζ : H} :
theorem is_primitive_root.fpow_eq_one {G₀ : Type u_4} {k : } {ζ : G₀} (h : k) :
ζ ^ k = 1
theorem is_primitive_root.fpow_eq_one_iff_dvd {G₀ : Type u_4} {k : } {ζ : G₀} (h : k) (l : ) :
ζ ^ l = 1 k l
theorem is_primitive_root.inv' {G₀ : Type u_4} {k : } {ζ : G₀} (h : k) :
@[simp]
theorem is_primitive_root.inv_iff' {G₀ : Type u_4} {k : } {ζ : G₀} :
theorem is_primitive_root.fpow_of_gcd_eq_one {G₀ : Type u_4} {k : } {ζ : G₀} (h : k) (i : ) (hi : i.gcd k = 1) :
@[simp]
theorem is_primitive_root.primitive_roots_zero {R : Type u_5}  :
@[simp]
theorem is_primitive_root.primitive_roots_one {R : Type u_5}  :
= {1}
theorem is_primitive_root.neg_one {R : Type u_5} (p : ) [ p] (hp : p 2) :
2
theorem is_primitive_root.eq_neg_one_of_two_right {R : Type u_5} {ζ : R} (h : 2) :
ζ = -1
theorem is_primitive_root.mem_roots_of_unity {R : Type u_5} {ζ : units R} {n : ℕ+} (h : n) :
ζ
def is_primitive_root.zmod_equiv_gpowers {R : Type u_5} {k : } {ζ : units R} (h : k) :

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

Equations
@[simp]
theorem is_primitive_root.zmod_equiv_gpowers_apply_coe_int {R : Type u_5} {k : } {ζ : units R} (h : k) (i : ) :
@[simp]
theorem is_primitive_root.zmod_equiv_gpowers_apply_coe_nat {R : Type u_5} {k : } {ζ : units R} (h : k) (i : ) :
@[simp]
theorem is_primitive_root.zmod_equiv_gpowers_symm_apply_gpow {R : Type u_5} {k : } {ζ : units R} (h : k) (i : ) :
@[simp]
theorem is_primitive_root.zmod_equiv_gpowers_symm_apply_gpow' {R : Type u_5} {k : } {ζ : units R} (h : k) (i : ) :
@[simp]
theorem is_primitive_root.zmod_equiv_gpowers_symm_apply_pow {R : Type u_5} {k : } {ζ : units R} (h : k) (i : ) :
@[simp]
theorem is_primitive_root.zmod_equiv_gpowers_symm_apply_pow' {R : Type u_5} {k : } {ζ : units R} (h : k) (i : ) :
theorem is_primitive_root.gpowers_eq {R : Type u_5} {k : ℕ+} {ζ : units R} (h : k) :
theorem is_primitive_root.eq_pow_of_mem_roots_of_unity {R : Type u_5} {k : ℕ+} {ζ ξ : units R} (h : k) (hξ : ξ ) :
∃ (i : ) (hi : i < k), ζ ^ i = ξ
theorem is_primitive_root.eq_pow_of_pow_eq_one {R : Type u_5} {k : } {ζ ξ : R} (h : k) (hξ : ξ ^ k = 1) (h0 : 0 < k) :
∃ (i : ) (H : i < k), ζ ^ i = ξ
theorem is_primitive_root.is_primitive_root_iff' {R : Type u_5} {k : ℕ+} {ζ ξ : units R} (h : k) :
∃ (i : ) (H : i < k) (hi : i.coprime k), ζ ^ i = ξ
theorem is_primitive_root.is_primitive_root_iff {R : Type u_5} {k : } {ζ ξ : R} (h : k) (h0 : 0 < k) :
∃ (i : ) (H : i < k) (hi : i.coprime k), ζ ^ i = ξ
theorem is_primitive_root.card_roots_of_unity' {R : Type u_5} {ζ : units R} {n : ℕ+} (h : n) :
= n
theorem is_primitive_root.card_roots_of_unity {R : Type u_5} {ζ : R} {n : ℕ+} (h : n) :
= n
theorem is_primitive_root.card_nth_roots {R : Type u_5} {ζ : R} {n : } (h : 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_5} {ζ : R} {n : } (h : 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_5} {ζ : R} {n : } (h : n) :
= n
theorem is_primitive_root.card_primitive_roots {R : Type u_5} {ζ : R} {k : } (h : k) (h0 : 0 < 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_5} {k l : } (hk : 0 < k) (hl : 0 < l) (h : k l) :
disjoint R) R)

The sets primitive_roots k R are pairwise disjoint.

theorem is_primitive_root.pow {R : Type u_5} {ζ : R} {n a b : } (hn : 0 < n) (h : n) (hprod : n = 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.nth_roots_one_eq_bUnion_primitive_roots' {R : Type u_5} {ζ : R} {n : ℕ+} (h : n) :
= n.divisors.bUnion (λ (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.

theorem is_primitive_root.nth_roots_one_eq_bUnion_primitive_roots {R : Type u_5} {ζ : R} {n : } (hpos : 0 < n) (h : n) :
= n.divisors.bUnion (λ (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.

theorem is_primitive_root.is_integral {n : } {K : Type u_7} [field K] {μ : K} (h : n) (hpos : 0 < n) :

μ is integral over ℤ.

theorem is_primitive_root.minpoly_dvd_X_pow_sub_one {n : } {K : Type u_7} [field K] {μ : K} (h : n) (hpos : 0 < n) [char_zero K] :
μ - 1

The minimal polynomial of a root of unity μ divides X ^ n - 1.

theorem is_primitive_root.separable_minpoly_mod {n : } {K : Type u_7} [field K] {μ : K} (h : n) (hpos : 0 < n) [char_zero K] {p : } [fact (nat.prime p)] (hdiv : ¬p n) :
μ)).separable

The reduction modulo p of the minimal polynomial of a root of unity μ is separable.

theorem is_primitive_root.squarefree_minpoly_mod {n : } {K : Type u_7} [field K] {μ : K} (h : n) (hpos : 0 < n) [char_zero K] {p : } [fact (nat.prime p)] (hdiv : ¬p n) :

The reduction modulo p of the minimal polynomial of a root of unity μ is squarefree.

theorem is_primitive_root.minpoly_dvd_expand {n : } {K : Type u_7} [field K] {μ : K} (h : n) (hpos : 0 < n) [char_zero K] {p : } (hprime : nat.prime p) (hdiv : ¬p n) :
μ ^ p))
theorem is_primitive_root.minpoly_dvd_pow_mod {n : } {K : Type u_7} [field K] {μ : K} (h : n) (hpos : 0 < n) [char_zero K] {p : } [hprime : fact (nat.prime p)] (hdiv : ¬p n) :
μ) ^ p)) ^ p
theorem is_primitive_root.minpoly_dvd_mod_p {n : } {K : Type u_7} [field K] {μ : K} (h : n) (hpos : 0 < n) [char_zero K] {p : } [hprime : fact (nat.prime p)] (hdiv : ¬p n) :
μ) ^ p))
theorem is_primitive_root.minpoly_eq_pow {n : } {K : Type u_7} [field K] {μ : K} (h : n) (hpos : 0 < n) [char_zero K] {p : } [hprime : fact (nat.prime p)] (hdiv : ¬p n) :
μ = ^ p)

If p is a prime that does not divide n, then the minimal polynomials of a primitive n-th root of unity μ and of μ ^ p are the same.

theorem is_primitive_root.minpoly_eq_pow_coprime {n : } {K : Type u_7} [field K] {μ : K} (h : n) (hpos : 0 < n) [char_zero K] {m : } (hcop : m.coprime n) :
μ = ^ m)

If m : ℕ is coprime with n, then the minimal polynomials of a primitive n-th root of unity μ and of μ ^ m are the same.

theorem is_primitive_root.pow_is_root_minpoly {n : } {K : Type u_7} [field K] {μ : K} (h : n) (hpos : 0 < n) [char_zero K] {m : } (hcop : m.coprime n) :
μ)).is_root ^ m)

If m : ℕ is coprime with n, then the minimal polynomial of a primitive n-th root of unity μ has μ ^ m as root.

theorem is_primitive_root.is_roots_of_minpoly {n : } {K : Type u_7} [field K] {μ : K} (h : n) (hpos : 0 < n) [char_zero K] :

primitive_roots n K is a subset of the roots of the minimal polynomial of a primitive n-th root of unity μ.

theorem is_primitive_root.totient_le_degree_minpoly {n : } {K : Type u_7} [field K] {μ : K} (h : n) (hpos : 0 < n) [char_zero K] :

The degree of the minimal polynomial of μ is at least totient n.