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 : Mˣ that satisfy m ^ k = 1

Equations
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ˣ) :
@[simp]
theorem roots_of_unity.coe_mk_of_pow_eq_coe {M : Type u_1} [comm_monoid M] (ζ : M) {n : ℕ+} (h : ζ ^ n = 1) :
def roots_of_unity.mk_of_pow_eq {M : Type u_1} [comm_monoid M] (ζ : M) {n : ℕ+} (h : ζ ^ n = 1) :

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
@[simp]
theorem roots_of_unity.coe_mk_of_pow_eq {M : Type u_1} [comm_monoid M] {ζ : M} {n : ℕ+} (h : ζ ^ n = 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 : Mˣ →* Nˣ) (k : ℕ+) :
@[norm_cast]
theorem roots_of_unity.coe_pow {R : Type u_5} {k : ℕ+} [comm_monoid R] (ζ : (roots_of_unity k R)) (m : ) :
^ m) = ζ ^ m
def restrict_roots_of_unity {R : Type u_5} {S : Type u_6} {F : Type u_7} [comm_semiring R] [comm_semiring S] [ring_hom_class F R S] (σ : F) (n : ℕ+) :

Restrict a ring homomorphism to the nth roots of unity

Equations
@[simp]
theorem restrict_roots_of_unity_coe_apply {R : Type u_5} {S : Type u_6} {F : Type u_7} {k : ℕ+} [comm_semiring R] [comm_semiring S] [ring_hom_class F R S] (σ : F) (ζ : (roots_of_unity k R)) :
def ring_equiv.restrict_roots_of_unity {R : Type u_5} {S : Type u_6} [comm_semiring R] [comm_semiring S] (σ : R ≃+* S) (n : ℕ+) :

Restrict a ring isomorphism 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 : ℕ+} [comm_semiring R] [comm_semiring S] (σ : R ≃+* S) (ζ : (roots_of_unity k R)) :
@[simp]
theorem ring_equiv.restrict_roots_of_unity_symm {R : Type u_5} {S : Type u_6} {k : ℕ+} [comm_semiring R] [comm_semiring S] (σ : R ≃+* S) :

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]
@[protected, instance]
noncomputable def roots_of_unity.fintype (R : Type u_5) (k : ℕ+) [comm_ring R] [is_domain R] :
Equations
@[protected, instance]
def roots_of_unity.is_cyclic (R : Type u_5) (k : ℕ+) [comm_ring R] [is_domain R] :
theorem card_roots_of_unity (R : Type u_5) (k : ℕ+) [comm_ring R] [is_domain R] :
theorem map_root_of_unity_eq_pow_self {R : Type u_5} {F : Type u_7} {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_5) [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 = 1k l

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

@[simp]
@[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) :
def is_primitive_root.to_roots_of_unity {M : Type u_1} [comm_monoid M] {μ : M} {n : ℕ+} (h : is_primitive_root μ n) :

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

Equations
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
@[simp]
theorem mem_primitive_roots {R : Type u_5} {k : } [comm_ring R] [is_domain R] {ζ : 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_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} :
@[simp]
theorem is_primitive_root.coe_units_iff {M : Type u_1} [comm_monoid M] {k : } {ζ : 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_of_prime {M : Type u_1} [comm_monoid M] {k : } {ζ : M} (h : is_primitive_root ζ 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 : is_primitive_root ζ k) (h0 : 0 < k) (i : ) :
@[protected]
theorem is_primitive_root.order_of {M : Type u_1} [comm_monoid M] (ζ : M) :
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 < ll < kζ ^ l 1
@[protected]
theorem is_primitive_root.not_iff {M : Type u_1} [comm_monoid M] {k : } {ζ : M} :
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) :
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) :

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.zero {M₀ : Type u_8} [comm_monoid_with_zero M₀] [nontrivial M₀] :
@[protected]
theorem is_primitive_root.ne_zero {k : } {M₀ : Type u_8} [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} [comm_group G] {k : } {ζ : G} (h : is_primitive_root ζ k) :
ζ ^ k = 1
theorem is_primitive_root.zpow_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.zpow_of_gcd_eq_one {G : Type u_3} [comm_group G] {k : } {ζ : G} (h : is_primitive_root ζ k) (i : ) (hi : i.gcd k = 1) :
theorem is_primitive_root.zpow_eq_one₀ {G₀ : Type u_4} [comm_group_with_zero G₀] {k : } {ζ : G₀} (h : is_primitive_root ζ k) :
ζ ^ k = 1
theorem is_primitive_root.zpow_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.zpow_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) :
theorem is_primitive_root.map_of_injective {R : Type u_5} {S : Type u_6} {F : Type u_7} {k : } [comm_semiring R] [comm_semiring S] {f : F} {ζ : R} [monoid_hom_class F R S] (h : is_primitive_root ζ k) (hf : function.injective f) :
theorem is_primitive_root.of_map_of_injective {R : Type u_5} {S : Type u_6} {F : Type u_7} {k : } [comm_semiring R] [comm_semiring S] {f : F} {ζ : R} [monoid_hom_class F R S] (h : is_primitive_root (f ζ) k) (hf : function.injective f) :
theorem is_primitive_root.map_iff_of_injective {R : Type u_5} {S : Type u_6} {F : Type u_7} {k : } [comm_semiring R] [comm_semiring S] {f : F} {ζ : R} [monoid_hom_class F R S] (hf : function.injective f) :
@[simp]
@[simp]
theorem is_primitive_root.primitive_roots_one {R : Type u_5} [comm_ring R] [is_domain R] :
theorem is_primitive_root.ne_zero' {R : Type u_5} {ζ : R} [comm_ring R] [is_domain R] {n : ℕ+} (hζ : is_primitive_root ζ n) :
theorem is_primitive_root.eq_neg_one_of_two_right {R : Type u_5} [comm_ring R] [no_zero_divisors R] {ζ : R} (h : is_primitive_root ζ 2) :
ζ = -1
theorem is_primitive_root.neg_one {R : Type u_5} [comm_ring R] (p : ) [nontrivial R] [h : char_p R p] (hp : p 2) :
noncomputable def is_primitive_root.zmod_equiv_zpowers {R : Type u_5} {k : } [comm_ring R] {ζ : Rˣ} (h : is_primitive_root ζ 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_zpowers_apply_coe_int {R : Type u_5} {k : } [comm_ring R] {ζ : Rˣ} (h : is_primitive_root ζ k) (i : ) :
@[simp]
theorem is_primitive_root.zmod_equiv_zpowers_apply_coe_nat {R : Type u_5} {k : } [comm_ring R] {ζ : Rˣ} (h : is_primitive_root ζ k) (i : ) :
@[simp]
theorem is_primitive_root.zmod_equiv_zpowers_symm_apply_zpow {R : Type u_5} {k : } [comm_ring R] {ζ : Rˣ} (h : is_primitive_root ζ k) (i : ) :
@[simp]
theorem is_primitive_root.zmod_equiv_zpowers_symm_apply_zpow' {R : Type u_5} {k : } [comm_ring R] {ζ : Rˣ} (h : is_primitive_root ζ k) (i : ) :
@[simp]
theorem is_primitive_root.zmod_equiv_zpowers_symm_apply_pow {R : Type u_5} {k : } [comm_ring R] {ζ : Rˣ} (h : is_primitive_root ζ k) (i : ) :
@[simp]
theorem is_primitive_root.zmod_equiv_zpowers_symm_apply_pow' {R : Type u_5} {k : } [comm_ring R] {ζ : Rˣ} (h : is_primitive_root ζ k) (i : ) :
theorem is_primitive_root.zpowers_eq {R : Type u_5} [comm_ring R] [is_domain R] {k : ℕ+} {ζ : Rˣ} (h : is_primitive_root ζ k) :
theorem is_primitive_root.eq_pow_of_mem_roots_of_unity {R : Type u_5} [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_5} [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_5} [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_5} [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_nth_roots {R : Type u_5} [comm_ring R] [is_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} [comm_ring R] [is_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} [comm_ring R] [is_domain R] {ζ : R} {n : } (h : is_primitive_root ζ n) :
theorem is_primitive_root.card_primitive_roots {R : Type u_5} [comm_ring R] [is_domain R] {ζ : R} {k : } (h : is_primitive_root ζ 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} [comm_ring R] [is_domain R] {k l : } (h : k l) :

The sets primitive_roots k R are pairwise disjoint.

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.

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_8} [comm_ring K] {μ : K} (h : is_primitive_root μ n) (hpos : 0 < n) :

μ is integral over .

theorem is_primitive_root.minpoly_dvd_X_pow_sub_one {n : } {K : Type u_8} [field K] {μ : K} (h : is_primitive_root μ n) [char_zero K] :

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

theorem is_primitive_root.separable_minpoly_mod {n : } {K : Type u_8} [field K] {μ : K} (h : is_primitive_root μ 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 separable.

theorem is_primitive_root.squarefree_minpoly_mod {n : } {K : Type u_8} [field K] {μ : K} (h : is_primitive_root μ 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_8} [field K] {μ : K} (h : is_primitive_root μ n) [char_zero K] {p : } (hprime : nat.prime p) (hdiv : ¬p n) :
theorem is_primitive_root.minpoly_dvd_pow_mod {n : } {K : Type u_8} [field K] {μ : K} (h : is_primitive_root μ n) [char_zero K] {p : } [hprime : fact (nat.prime p)] (hdiv : ¬p n) :
theorem is_primitive_root.minpoly_dvd_mod_p {n : } {K : Type u_8} [field K] {μ : K} (h : is_primitive_root μ n) [char_zero K] {p : } [hprime : fact (nat.prime p)] (hdiv : ¬p n) :
theorem is_primitive_root.minpoly_eq_pow {n : } {K : Type u_8} [field K] {μ : K} (h : is_primitive_root μ n) [char_zero K] {p : } [hprime : fact (nat.prime p)] (hdiv : ¬p n) :
minpoly μ = minpoly ^ 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_8} [field K] {μ : K} (h : is_primitive_root μ n) [char_zero K] {m : } (hcop : m.coprime n) :
minpoly μ = minpoly ^ 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_8} [field K] {μ : K} (h : is_primitive_root μ n) [char_zero K] {m : } (hcop : m.coprime n) :

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

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_8} [field K] {μ : K} (h : is_primitive_root μ n) [char_zero K] :

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

theorem is_primitive_root.coe_inv_aut_to_pow_apply (R : Type u_5) {S : Type u_6} [comm_ring S] [is_domain S] {μ : S} {n : ℕ+} (hμ : is_primitive_root μ n) [comm_ring R] [algebra R S] (g : S ≃ₐ[R] S) :
theorem is_primitive_root.coe_aut_to_pow_apply (R : Type u_5) {S : Type u_6} [comm_ring S] [is_domain S] {μ : S} {n : ℕ+} (hμ : is_primitive_root μ n) [comm_ring R] [algebra R S] (g : S ≃ₐ[R] S) :
noncomputable def is_primitive_root.aut_to_pow (R : Type u_5) {S : Type u_6} [comm_ring S] [is_domain S] {μ : S} {n : ℕ+} (hμ : is_primitive_root μ n) [comm_ring R] [algebra R S] :

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

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