# Minimal polynomial of roots of unity #

We gather several results about minimal polynomial of root of unity.

## Main results #

• IsPrimitiveRoot.totient_le_degree_minpoly: The degree of the minimal polynomial of an n-th primitive root of unity is at least totient n.
theorem IsPrimitiveRoot.isIntegral {n : } {K : Type u_1} [] {μ : K} (h : ) (hpos : 0 < n) :

μ is integral over ℤ.

theorem IsPrimitiveRoot.minpoly_dvd_x_pow_sub_one {n : } {K : Type u_1} [] {μ : K} (h : ) [] [] :
Polynomial.X ^ n - 1

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

theorem IsPrimitiveRoot.separable_minpoly_mod {n : } {K : Type u_1} [] {μ : K} (h : ) [] [] {p : } [Fact (Nat.Prime p)] (hdiv : ¬p n) :

The reduction modulo p of the minimal polynomial of a root of unity μ is separable.

theorem IsPrimitiveRoot.squarefree_minpoly_mod {n : } {K : Type u_1} [] {μ : K} (h : ) [] [] {p : } [Fact (Nat.Prime p)] (hdiv : ¬p n) :

The reduction modulo p of the minimal polynomial of a root of unity μ is squarefree.

theorem IsPrimitiveRoot.minpoly_dvd_expand {n : } {K : Type u_1} [] {μ : K} (h : ) [] [] {p : } (hdiv : ¬p n) :
(minpoly (μ ^ p))

Let P be the minimal polynomial of a root of unity μ and Q be the minimal polynomial of μ ^ p, where p is a natural number that does not divide n. Then P divides expand ℤ p Q.

theorem IsPrimitiveRoot.minpoly_dvd_pow_mod {n : } {K : Type u_1} [] {μ : K} (h : ) [] [] {p : } [hprime : Fact (Nat.Prime p)] (hdiv : ¬p n) :

Let P be the minimal polynomial of a root of unity μ and Q be the minimal polynomial of μ ^ p, where p is a prime that does not divide n. Then P divides Q ^ p modulo p.

theorem IsPrimitiveRoot.minpoly_dvd_mod_p {n : } {K : Type u_1} [] {μ : K} (h : ) [] [] {p : } [Fact (Nat.Prime p)] (hdiv : ¬p n) :

Let P be the minimal polynomial of a root of unity μ and Q be the minimal polynomial of μ ^ p, where p is a prime that does not divide n. Then P divides Q modulo p.

theorem IsPrimitiveRoot.minpoly_eq_pow {n : } {K : Type u_1} [] {μ : K} (h : ) [] [] {p : } [hprime : Fact (Nat.Prime p)] (hdiv : ¬p n) :
= 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 IsPrimitiveRoot.minpoly_eq_pow_coprime {n : } {K : Type u_1} [] {μ : K} (h : ) [] [] {m : } (hcop : m.Coprime n) :
= 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 IsPrimitiveRoot.pow_isRoot_minpoly {n : } {K : Type u_1} [] {μ : K} (h : ) [] [] {m : } (hcop : m.Coprime n) :
(Polynomial.map (minpoly μ)).IsRoot (μ ^ m)

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

theorem IsPrimitiveRoot.is_roots_of_minpoly {n : } {K : Type u_1} [] {μ : K} (h : ) [] [] [] :
(Polynomial.map (minpoly μ)).roots.toFinset

primitiveRoots n K is a subset of the roots of the minimal polynomial of a primitive n-th root of unity μ.

theorem IsPrimitiveRoot.totient_le_degree_minpoly {n : } {K : Type u_1} [] {μ : K} (h : ) [] [] :
n.totient (minpoly μ).natDegree

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