mathlib documentation

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

Main results

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) :
ζ roots_of_unity k 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 : units M →* units N) (k : ℕ+) :

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

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) [integral_domain R] :

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} [integral_domain R] {k : } {ζ : R} (h0 : 0 < k) :

theorem is_primitive_root.iff_def {M : Type u_1} [comm_monoid M] (ζ : M) (k : ) :
is_primitive_root ζ 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 : 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.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] :

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

@[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 : is_primitive_root ζ k) (i : ) (hi : i.coprime 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 : ) :

theorem is_primitive_root.gpow_eq_one {G : Type u_3} [comm_group G] {k : } {ζ : G} (h : is_primitive_root ζ k) :
ζ ^ k = 1

theorem is_primitive_root.gpow_eq_one_iff_dvd {G : Type u_3} [comm_group G] {k : } {ζ : G} (h : is_primitive_root ζ k) (l : ) :
ζ ^ l = 1 k l

theorem is_primitive_root.inv {G : Type u_3} [comm_group G] {k : } {ζ : G} (h : is_primitive_root ζ 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 : is_primitive_root ζ 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} [comm_group_with_zero G₀] {k : } {ζ : G₀} (h : is_primitive_root ζ k) :
ζ ^ k = 1

theorem is_primitive_root.fpow_eq_one_iff_dvd {G₀ : Type u_4} [comm_group_with_zero G₀] {k : } {ζ : G₀} (h : is_primitive_root ζ k) (l : ) :
ζ ^ l = 1 k l

theorem is_primitive_root.inv' {G₀ : Type u_4} [comm_group_with_zero G₀] {k : } {ζ : G₀} (h : is_primitive_root ζ k) :

@[simp]
theorem is_primitive_root.inv_iff' {G₀ : Type u_4} [comm_group_with_zero G₀] {k : } {ζ : G₀} :

theorem is_primitive_root.fpow_of_gcd_eq_one {G₀ : Type u_4} [comm_group_with_zero G₀] {k : } {ζ : G₀} (h : is_primitive_root ζ k) (i : ) (hi : i.gcd k = 1) :

@[simp]

theorem is_primitive_root.neg_one {R : Type u_5} [integral_domain R] (p : ) [char_p R p] (hp : p 2) :

theorem is_primitive_root.eq_neg_one_of_two_right {R : Type u_5} [integral_domain R] {ζ : R} (h : is_primitive_root ζ 2) :
ζ = -1

theorem is_primitive_root.mem_roots_of_unity {R : Type u_5} [integral_domain R] {ζ : units R} {n : ℕ+} (h : is_primitive_root ζ n) :

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

Equations
@[simp]

@[simp]

@[simp]

@[simp]
theorem is_primitive_root.zmod_equiv_gpowers_symm_apply_gpow' {R : Type u_5} [integral_domain R] {k : } {ζ : units R} (h : is_primitive_root ζ k) (i : ) :

@[simp]

@[simp]
theorem is_primitive_root.zmod_equiv_gpowers_symm_apply_pow' {R : Type u_5} [integral_domain R] {k : } {ζ : units R} (h : is_primitive_root ζ k) (i : ) :

theorem is_primitive_root.gpowers_eq {R : Type u_5} [integral_domain R] {k : ℕ+} {ζ : units R} (h : is_primitive_root ζ k) :

theorem is_primitive_root.eq_pow_of_mem_roots_of_unity {R : Type u_5} [integral_domain R] {k : ℕ+} {ζ ξ : units 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_5} [integral_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_5} [integral_domain R] {k : ℕ+} {ζ ξ : units 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_5} [integral_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_nth_roots {R : Type u_5} [integral_domain R] {ζ : R} {n : } (h : is_primitive_root ζ 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} [integral_domain R] {ζ : R} {n : } (h : is_primitive_root ζ n) :

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} [integral_domain R] {ζ : R} {n : } (h : is_primitive_root ζ n) :

theorem is_primitive_root.card_primitive_roots {R : Type u_5} [integral_domain R] {ζ : R} {k : } (h : is_primitive_root ζ k) (h0 : 0 < k) :

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} [integral_domain R] {k l : } (hk : 0 < k) (hl : 0 < l) (h : k l) :

The sets primitive_roots k R are pairwise disjoint.

theorem is_primitive_root.pow {R : Type u_5} [integral_domain R] {ζ : R} {n a b : } (hn : 0 < n) (h : is_primitive_root ζ 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.

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} [integral_domain R] {ζ : R} {n : } (hpos : 0 < n) (h : is_primitive_root ζ n) :

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.