# 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`.

source
theorem IsPrimitiveRoot.isIntegral {n : ℕ} {K : Type u_1} [CommRing K] {μ : K} (h : IsPrimitiveRoot μ n) (hpos : 0 < n) :
IsIntegral ℤ μ

`μ` is integral over `ℤ`.

source
theorem IsPrimitiveRoot.minpoly_dvd_x_pow_sub_one {n : ℕ} {K : Type u_1} [CommRing K] {μ : K} (h : IsPrimitiveRoot μ n) [IsDomain K] [CharZero K] :
minpoly ℤ μ ∣ Polynomial.X ^ n - 1

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

source
theorem IsPrimitiveRoot.separable_minpoly_mod {n : ℕ} {K : Type u_1} [CommRing K] {μ : K} (h : IsPrimitiveRoot μ n) [IsDomain K] [CharZero K] {p : ℕ} [Fact (Nat.Prime p)] (hdiv : ¬p ∣ n) :
(Polynomial.map (Int.castRingHom (ZMod p)) (minpoly ℤ μ)).Separable

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

source
theorem IsPrimitiveRoot.squarefree_minpoly_mod {n : ℕ} {K : Type u_1} [CommRing K] {μ : K} (h : IsPrimitiveRoot μ n) [IsDomain K] [CharZero K] {p : ℕ} [Fact (Nat.Prime p)] (hdiv : ¬p ∣ n) :
Squarefree (Polynomial.map (Int.castRingHom (ZMod p)) (minpoly ℤ μ))

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

source
theorem IsPrimitiveRoot.minpoly_dvd_expand {n : ℕ} {K : Type u_1} [CommRing K] {μ : K} (h : IsPrimitiveRoot μ n) [IsDomain K] [CharZero K] {p : ℕ} (hdiv : ¬p ∣ n) :
minpoly ℤ μ ∣ (Polynomial.expand ℤ p) (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`.

source
theorem IsPrimitiveRoot.minpoly_dvd_pow_mod {n : ℕ} {K : Type u_1} [CommRing K] {μ : K} (h : IsPrimitiveRoot μ n) [IsDomain K] [CharZero K] {p : ℕ} [hprime : Fact (Nat.Prime p)] (hdiv : ¬p ∣ n) :
Polynomial.map (Int.castRingHom (ZMod p)) (minpoly ℤ μ) ∣ Polynomial.map (Int.castRingHom (ZMod p)) (minpoly ℤ (μ ^ p)) ^ p

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

source
theorem IsPrimitiveRoot.minpoly_dvd_mod_p {n : ℕ} {K : Type u_1} [CommRing K] {μ : K} (h : IsPrimitiveRoot μ n) [IsDomain K] [CharZero K] {p : ℕ} [Fact (Nat.Prime p)] (hdiv : ¬p ∣ n) :
Polynomial.map (Int.castRingHom (ZMod p)) (minpoly ℤ μ) ∣ Polynomial.map (Int.castRingHom (ZMod p)) (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 prime that does not divide `n`. Then `P` divides `Q` modulo `p`.

source
theorem IsPrimitiveRoot.minpoly_eq_pow {n : ℕ} {K : Type u_1} [CommRing K] {μ : K} (h : IsPrimitiveRoot μ n) [IsDomain K] [CharZero 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.

source
theorem IsPrimitiveRoot.minpoly_eq_pow_coprime {n : ℕ} {K : Type u_1} [CommRing K] {μ : K} (h : IsPrimitiveRoot μ n) [IsDomain K] [CharZero 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.

source
theorem IsPrimitiveRoot.pow_isRoot_minpoly {n : ℕ} {K : Type u_1} [CommRing K] {μ : K} (h : IsPrimitiveRoot μ n) [IsDomain K] [CharZero K] {m : ℕ} (hcop : m.Coprime n) :
(Polynomial.map (Int.castRingHom K) (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.

source
theorem IsPrimitiveRoot.is_roots_of_minpoly {n : ℕ} {K : Type u_1} [CommRing K] {μ : K} (h : IsPrimitiveRoot μ n) [IsDomain K] [CharZero K] [DecidableEq K] :
primitiveRoots n K ⊆ (Polynomial.map (Int.castRingHom K) (minpoly ℤ μ)).roots.toFinset

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

source
theorem IsPrimitiveRoot.totient_le_degree_minpoly {n : ℕ} {K : Type u_1} [CommRing K] {μ : K} (h : IsPrimitiveRoot μ n) [IsDomain K] [CharZero K] :
n.totient ≤ (minpoly ℤ μ).natDegree

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