# Roots of cyclotomic polynomials. #

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 #

- `IsPrimitiveRoot.isRoot_cyclotomic` : Any `n`-th primitive root of unity is a root of `cyclotomic n R`.
- `isRoot_cyclotomic_iff` : if `NeZero (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`.

source
theorem Polynomial.isRoot_of_unity_of_root_cyclotomic {R : Type u_1} [CommRing R] {n : ℕ} {ζ : R} {i : ℕ} (hi : i ∈ n.divisors) (h : (cyclotomic i R).IsRoot ζ) :
ζ ^ n = 1
source
theorem isRoot_of_unity_iff {n : ℕ} (h : 0 < n) (R : Type u_2) [CommRing R] [IsDomain R] {ζ : R} :
ζ ^ n = 1 ↔ ∃ i ∈ n.divisors, (Polynomial.cyclotomic i R).IsRoot ζ
source
theorem IsPrimitiveRoot.isRoot_cyclotomic {R : Type u_1} [CommRing R] {n : ℕ} [IsDomain R] (hpos : 0 < n) {μ : R} (h : IsPrimitiveRoot μ n) :
(Polynomial.cyclotomic n R).IsRoot μ

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

source
theorem Polynomial.isRoot_cyclotomic_iff {R : Type u_1} [CommRing R] {n : ℕ} [IsDomain R] [NeZero ↑n] {μ : R} :
(cyclotomic n R).IsRoot μ ↔ IsPrimitiveRoot μ n
source
theorem Polynomial.roots_cyclotomic_nodup {R : Type u_1} [CommRing R] {n : ℕ} [IsDomain R] [NeZero ↑n] :
(cyclotomic n R).roots.Nodup
source
theorem Polynomial.cyclotomic.roots_to_finset_eq_primitiveRoots {R : Type u_1} [CommRing R] {n : ℕ} [IsDomain R] [NeZero ↑n] :
{ val := (cyclotomic n R).roots, nodup := ⋯ } = primitiveRoots n R
source
theorem Polynomial.cyclotomic.roots_eq_primitiveRoots_val {R : Type u_1} [CommRing R] {n : ℕ} [IsDomain R] [NeZero ↑n] :
(cyclotomic n R).roots = (primitiveRoots n R).val
source
theorem Polynomial.isRoot_cyclotomic_iff_charZero {n : ℕ} {R : Type u_2} [CommRing R] [IsDomain R] [CharZero R] {μ : R} (hn : 0 < n) :
(cyclotomic n R).IsRoot μ ↔ IsPrimitiveRoot μ 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.

source
theorem Polynomial.cyclotomic_injective {R : Type u_1} [CommRing R] [CharZero R] :
Function.Injective fun (n : ℕ) => cyclotomic n R

Over a ring `R` of characteristic zero, `fun n => cyclotomic n R` is injective.

source
theorem IsPrimitiveRoot.minpoly_dvd_cyclotomic {n : ℕ} {K : Type u_2} [Field K] {μ : K} (h : IsPrimitiveRoot μ n) (hpos : 0 < n) [CharZero K] :
minpoly ℤ μ ∣ Polynomial.cyclotomic n ℤ

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

source
theorem IsPrimitiveRoot.minpoly_eq_cyclotomic_of_irreducible {K : Type u_2} [Field K] {R : Type u_3} [CommRing R] [IsDomain R] {μ : R} {n : ℕ} [Algebra K R] (hμ : IsPrimitiveRoot μ n) (h : Irreducible (Polynomial.cyclotomic n K)) [NeZero ↑n] :
Polynomial.cyclotomic n K = minpoly K μ
source
theorem Polynomial.cyclotomic_eq_minpoly {n : ℕ} {K : Type u_2} [Field K] {μ : K} (h : IsPrimitiveRoot μ n) (hpos : 0 < n) [CharZero K] :
cyclotomic n ℤ = minpoly ℤ μ

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

source
theorem Polynomial.cyclotomic_eq_minpoly_rat {n : ℕ} {K : Type u_2} [Field K] {μ : K} (h : IsPrimitiveRoot μ n) (hpos : 0 < n) [CharZero K] :
cyclotomic n ℚ = minpoly ℚ μ

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

source
theorem Polynomial.cyclotomic.irreducible {n : ℕ} (hpos : 0 < n) :
Irreducible (cyclotomic n ℤ)

`cyclotomic n ℤ` is irreducible.

source
theorem Polynomial.cyclotomic.irreducible_rat {n : ℕ} (hpos : 0 < n) :
Irreducible (cyclotomic n ℚ)

`cyclotomic n ℚ` is irreducible.

source
theorem Polynomial.cyclotomic.isCoprime_rat {n m : ℕ} (h : n ≠ m) :
IsCoprime (cyclotomic n ℚ) (cyclotomic m ℚ)

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