mathlib3 documentation

ring_theory.polynomial.cyclotomic.roots

Roots of cyclotomic polynomials. #

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

We gather results about roots of cyclotomic polynomials. In particular we show in polynomial.cyclotomic_eq_minpoly that cyclotomic n R is the minimal polynomial of a primitive root of unity.

Main results #

is_primitive_root.is_root_cyclotomic : Any n-th primitive root of unity is a root of cyclotomic n R.
is_root_cyclotomic_iff : if ne_zero (n : R), then μ is a root of cyclotomic n R if and only if μ is a primitive root of unity.
polynomial.cyclotomic_eq_minpoly : cyclotomic n ℤ is the minimal polynomial of a primitive n-th root of unity μ.
polynomial.cyclotomic.irreducible : cyclotomic n ℤ is irreducible.

Implementation details #

To prove polynomial.cyclotomic.irreducible, the irreducibility of cyclotomic n ℤ, we show in polynomial.cyclotomic_eq_minpoly that cyclotomic n ℤ is the minimal polynomial of any n-th primitive root of unity μ : K, where K is a field of characteristic 0.

theorem polynomial.is_root_of_unity_of_root_cyclotomic {R : Type u_1} [comm_ring R] {n : ℕ} {ζ : R} {i : ℕ} (hi : i ∈ n.divisors) (h : (polynomial.cyclotomic i R).is_root ζ) :

ζ ^ n = 1

theorem is_root_of_unity_iff {n : ℕ} (h : 0 < n) (R : Type u_1) [comm_ring R] [is_domain R] {ζ : R} :

ζ ^ n = 1 ↔ ∃ (i : ℕ) (H : i ∈ n.divisors), (polynomial.cyclotomic i R).is_root ζ

theorem is_primitive_root.is_root_cyclotomic {R : Type u_1} [comm_ring R] {n : ℕ} [is_domain R] (hpos : 0 < n) {μ : R} (h : is_primitive_root μ n) :

(polynomial.cyclotomic n R).is_root μ

Any n-th primitive root of unity is a root of cyclotomic n R.

theorem polynomial.is_root_cyclotomic_iff {R : Type u_1} [comm_ring R] {n : ℕ} [is_domain R] [ne_zero ↑n] {μ : R} :

(polynomial.cyclotomic n R).is_root μ ↔ is_primitive_root μ n

theorem polynomial.roots_cyclotomic_nodup {R : Type u_1} [comm_ring R] {n : ℕ} [is_domain R] [ne_zero ↑n] :

(polynomial.cyclotomic n R).roots.nodup

theorem polynomial.cyclotomic.roots_to_finset_eq_primitive_roots {R : Type u_1} [comm_ring R] {n : ℕ} [is_domain R] [ne_zero ↑n] :

{val := (polynomial.cyclotomic n R).roots, nodup := _} = primitive_roots n R

theorem polynomial.cyclotomic.roots_eq_primitive_roots_val {R : Type u_1} [comm_ring R] {n : ℕ} [is_domain R] [ne_zero ↑n] :

(polynomial.cyclotomic n R).roots = (primitive_roots n R).val

theorem polynomial.is_root_cyclotomic_iff_char_zero {n : ℕ} {R : Type u_1} [comm_ring R] [is_domain R] [char_zero R] {μ : R} (hn : 0 < n) :

(polynomial.cyclotomic n R).is_root μ ↔ is_primitive_root μ n

If R is of characteristic zero, then ζ is a root of cyclotomic n R if and only if it is a primitive n-th root of unity.

theorem polynomial.cyclotomic_injective {R : Type u_1} [comm_ring R] [char_zero R] :

function.injective (λ (n : ℕ), polynomial.cyclotomic n R)

Over a ring R of characteristic zero, λ n, cyclotomic n R is injective.

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

minpoly ℤ μ ∣ polynomial.cyclotomic n ℤ

The minimal polynomial of a primitive n-th root of unity μ divides cyclotomic n ℤ.

theorem is_primitive_root.minpoly_eq_cyclotomic_of_irreducible {K : Type u_1} [field K] {R : Type u_2} [comm_ring R] [is_domain R] {μ : R} {n : ℕ} [algebra K R] (hμ : is_primitive_root μ n) (h : irreducible (polynomial.cyclotomic n K)) [ne_zero ↑n] :

polynomial.cyclotomic n K = minpoly K μ

theorem polynomial.cyclotomic_eq_minpoly {n : ℕ} {K : Type u_1} [field K] {μ : K} (h : is_primitive_root μ n) (hpos : 0 < n) [char_zero K] :

polynomial.cyclotomic n ℤ = minpoly ℤ μ

cyclotomic n ℤ is the minimal polynomial of a primitive n-th root of unity μ.

theorem polynomial.cyclotomic_eq_minpoly_rat {n : ℕ} {K : Type u_1} [field K] {μ : K} (h : is_primitive_root μ n) (hpos : 0 < n) [char_zero K] :

polynomial.cyclotomic n ℚ = minpoly ℚ μ

cyclotomic n ℚ is the minimal polynomial of a primitive n-th root of unity μ.

theorem polynomial.cyclotomic.irreducible {n : ℕ} (hpos : 0 < n) :

irreducible (polynomial.cyclotomic n ℤ)

cyclotomic n ℤ is irreducible.

theorem polynomial.cyclotomic.irreducible_rat {n : ℕ} (hpos : 0 < n) :

irreducible (polynomial.cyclotomic n ℚ)

cyclotomic n ℚ is irreducible.

theorem polynomial.cyclotomic.is_coprime_rat {n m : ℕ} (h : n ≠ m) :

is_coprime (polynomial.cyclotomic n ℚ) (polynomial.cyclotomic m ℚ)

If n ≠ m, then (cyclotomic n ℚ) and (cyclotomic m ℚ) are coprime.