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.

theorem Polynomial.isRoot_of_unity_of_root_cyclotomic {R : Type u_1} [CommRing R] {n : ℕ} {ζ : R} {i : ℕ} (hi : i ∈ Nat.divisors n) (h : Polynomial.IsRoot (Polynomial.cyclotomic i R) ζ) : ζ ^ n = 1

theorem isRoot_of_unity_iff {n : ℕ} (h : 0 < n) (R : Type u_2) [CommRing R] [IsDomain R] {ζ : R} : ζ ^ n = 1 ↔ ∃ i ∈ Nat.divisors n, Polynomial.IsRoot (Polynomial.cyclotomic i R) ζ

theorem IsPrimitiveRoot.isRoot_cyclotomic {R : Type u_1} [CommRing R] {n : ℕ} [IsDomain R] (hpos : 0 < n) {μ : R} (h : IsPrimitiveRoot μ n) : Polynomial.IsRoot (Polynomial.cyclotomic n R) μ

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

theorem Polynomial.isRoot_cyclotomic_iff {R : Type u_1} [CommRing R] {n : ℕ} [IsDomain R] [NeZero ↑n] {μ : R} : Polynomial.IsRoot (Polynomial.cyclotomic n R) μ ↔ IsPrimitiveRoot μ n

theorem Polynomial.roots_cyclotomic_nodup {R : Type u_1} [CommRing R] {n : ℕ} [IsDomain R] [NeZero ↑n] : Multiset.Nodup (Polynomial.roots (Polynomial.cyclotomic n R))

theorem Polynomial.cyclotomic.roots_to_finset_eq_primitiveRoots {R : Type u_1} [CommRing R] {n : ℕ} [IsDomain R] [NeZero ↑n] : { val := Polynomial.roots (Polynomial.cyclotomic n R), nodup := ⋯ } = primitiveRoots n R

theorem Polynomial.cyclotomic.roots_eq_primitiveRoots_val {R : Type u_1} [CommRing R] {n : ℕ} [IsDomain R] [NeZero ↑n] : Polynomial.roots (Polynomial.cyclotomic n R) = (primitiveRoots n R).val

theorem Polynomial.isRoot_cyclotomic_iff_charZero {n : ℕ} {R : Type u_2} [CommRing R] [IsDomain R] [CharZero R] {μ : R} (hn : 0 < n) : Polynomial.IsRoot (Polynomial.cyclotomic n R) μ ↔ 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.

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

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

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 ℤ.

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 μ

theorem Polynomial.cyclotomic_eq_minpoly {n : ℕ} {K : Type u_2} [Field K] {μ : K} (h : IsPrimitiveRoot μ n) (hpos : 0 < n) [CharZero 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_2} [Field K] {μ : K} (h : IsPrimitiveRoot μ n) (hpos : 0 < n) [CharZero 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.isCoprime_rat {n : ℕ} {m : ℕ} (h : n ≠ m) : IsCoprime (Polynomial.cyclotomic n ℚ) (Polynomial.cyclotomic m ℚ)

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