mathlib3 documentation

ring_theory.roots_of_unity.minpoly

Minimal polynomial of roots of unity #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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

Main results #

source
theorem is_primitive_root.is_integral {n : ℕ} {K : Type u_1} [comm_ring K] {μ : K} (h : is_primitive_root μ n) (hpos : 0 < n) :
is_integral ℤ μ

μ is integral over ℤ.

source
theorem is_primitive_root.minpoly_dvd_X_pow_sub_one {n : ℕ} {K : Type u_1} [comm_ring K] {μ : K} (h : is_primitive_root μ n) [is_domain K] [char_zero K] :
minpoly ℤ μ ∣ polynomial.X ^ n - 1

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

source
theorem is_primitive_root.separable_minpoly_mod {n : ℕ} {K : Type u_1} [comm_ring K] {μ : K} (h : is_primitive_root μ n) [is_domain K] [char_zero K] {p : ℕ} [fact (nat.prime p)] (hdiv : ¬p ∣ n) :
(polynomial.map (int.cast_ring_hom (zmod p)) (minpoly ℤ μ)).separable

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

source
theorem is_primitive_root.squarefree_minpoly_mod {n : ℕ} {K : Type u_1} [comm_ring K] {μ : K} (h : is_primitive_root μ n) [is_domain K] [char_zero K] {p : ℕ} [fact (nat.prime p)] (hdiv : ¬p ∣ n) :
squarefree (polynomial.map (int.cast_ring_hom (zmod p)) (minpoly ℤ μ))

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

source
theorem is_primitive_root.minpoly_dvd_expand {n : ℕ} {K : Type u_1} [comm_ring K] {μ : K} (h : is_primitive_root μ n) [is_domain K] [char_zero K] {p : ℕ} (hdiv : ¬p ∣ n) :
minpoly ℤ μ ∣ ⇑(polynomial.expand ℤ p) (minpoly ℤ (μ ^ p))
source
theorem is_primitive_root.minpoly_dvd_pow_mod {n : ℕ} {K : Type u_1} [comm_ring K] {μ : K} (h : is_primitive_root μ n) [is_domain K] [char_zero K] {p : ℕ} [hprime : fact (nat.prime p)] (hdiv : ¬p ∣ n) :
polynomial.map (int.cast_ring_hom (zmod p)) (minpoly ℤ μ) ∣ polynomial.map (int.cast_ring_hom (zmod p)) (minpoly ℤ (μ ^ p)) ^ p
source
theorem is_primitive_root.minpoly_dvd_mod_p {n : ℕ} {K : Type u_1} [comm_ring K] {μ : K} (h : is_primitive_root μ n) [is_domain K] [char_zero K] {p : ℕ} [hprime : fact (nat.prime p)] (hdiv : ¬p ∣ n) :
polynomial.map (int.cast_ring_hom (zmod p)) (minpoly ℤ μ) ∣ polynomial.map (int.cast_ring_hom (zmod p)) (minpoly ℤ (μ ^ p))
source
theorem is_primitive_root.minpoly_eq_pow {n : ℕ} {K : Type u_1} [comm_ring K] {μ : K} (h : is_primitive_root μ n) [is_domain K] [char_zero 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 is_primitive_root.minpoly_eq_pow_coprime {n : ℕ} {K : Type u_1} [comm_ring K] {μ : K} (h : is_primitive_root μ n) [is_domain K] [char_zero 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 is_primitive_root.pow_is_root_minpoly {n : ℕ} {K : Type u_1} [comm_ring K] {μ : K} (h : is_primitive_root μ n) [is_domain K] [char_zero K] {m : ℕ} (hcop : m.coprime n) :
(polynomial.map (int.cast_ring_hom K) (minpoly ℤ μ)).is_root (μ ^ 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 is_primitive_root.is_roots_of_minpoly {n : ℕ} {K : Type u_1} [comm_ring K] {μ : K} (h : is_primitive_root μ n) [is_domain K] [char_zero K] [decidable_eq K] :
primitive_roots n K ⊆ (polynomial.map (int.cast_ring_hom K) (minpoly ℤ μ)).roots.to_finset

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

source
theorem is_primitive_root.totient_le_degree_minpoly {n : ℕ} {K : Type u_1} [comm_ring K] {μ : K} (h : is_primitive_root μ n) [is_domain K] [char_zero K] :
n.totient ≤ (minpoly ℤ μ).nat_degree

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