# 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 : ℕ+) :

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_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) :
1).card = 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_bind_primitive_roots' {R : Type u_5} {ζ : R} {n : ℕ+} (h : n) :
= n.divisors.bind (λ (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_bind_primitive_roots {R : Type u_5} {ζ : R} {n : } (hpos : 0 < n) (h : n) :
= n.divisors.bind (λ (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.