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} [CommRing K] {μ : K} (h : IsPrimitiveRoot μ n) (hpos : 0 < n) : IsIntegral ℤ μ

μ is integral over ℤ.

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.

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.Separable (Polynomial.map (Int.castRingHom (ZMod p)) (minpoly ℤ μ))

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} [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.

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))

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

theorem IsPrimitiveRoot.minpoly_dvd_mod_p {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))

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.

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

theorem IsPrimitiveRoot.pow_isRoot_minpoly {n : ℕ} {K : Type u_1} [CommRing K] {μ : K} (h : IsPrimitiveRoot μ n) [IsDomain K] [CharZero K] {m : ℕ} (hcop : Nat.Coprime m n) : Polynomial.IsRoot (Polynomial.map (Int.castRingHom K) (minpoly ℤ μ)) (μ ^ 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} [CommRing K] {μ : K} (h : IsPrimitiveRoot μ n) [IsDomain K] [CharZero K] [DecidableEq K] : primitiveRoots n K ⊆ Multiset.toFinset (Polynomial.roots (Polynomial.map (Int.castRingHom K) (minpoly ℤ μ)))

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} [CommRing K] {μ : K} (h : IsPrimitiveRoot μ n) [IsDomain K] [CharZero K] : Nat.totient n ≤ Polynomial.natDegree (minpoly ℤ μ)

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