From d21d17b1092cf495316e68cf285c0a561de5157e Mon Sep 17 00:00:00 2001 From: Riccardo Brasca Date: Tue, 15 Dec 2020 13:31:17 +0000 Subject: [PATCH] feat(ring_theory/roots_of_unity): minimal polynomial of primitive roots (#5322) I've added some simple results about the minimal polynomial of a primitive root of unity. The next step will be to prove that any two primitive roots have the same minimal polynomial. --- src/ring_theory/roots_of_unity.lean | 33 +++++++++++++++++++++++++++++ 1 file changed, 33 insertions(+) diff --git a/src/ring_theory/roots_of_unity.lean b/src/ring_theory/roots_of_unity.lean index d213ba24b068c..e7f1ce513aa98 100644 --- a/src/ring_theory/roots_of_unity.lean +++ b/src/ring_theory/roots_of_unity.lean @@ -11,6 +11,7 @@ import ring_theory.integral_domain import number_theory.divisors import data.zmod.basic import tactic.zify +import field_theory.separable /-! # Roots of unity and primitive roots of unity @@ -715,4 +716,36 @@ lemma nth_roots_one_eq_bind_primitive_roots {ζ : R} {n : ℕ} (hpos : 0 < n) end integral_domain +section minimal_polynomial + +open minimal_polynomial + +variables {n : ℕ} {K : Type*} [field K] {μ : K} (h : is_primitive_root μ n) (hpos : 0 < n) + +include n μ h hpos + +/--`μ` is integral over `ℤ`. -/ +lemma is_integral : is_integral ℤ μ := +begin + use (X ^ n - 1), + split, + { exact (monic_X_pow_sub_C 1 (ne_of_lt hpos).symm) }, + { simp only [((is_primitive_root.iff_def μ n).mp h).left, eval₂_one, eval₂_X_pow, eval₂_sub, + sub_self] } +end + +variables [char_zero K] + +/--The minimal polynomial of `μ` divides `X ^ n - 1`. -/ +lemma minimal_polynomial_dvd_X_pow_sub_one : + minimal_polynomial (is_integral h hpos) ∣ X ^ n - 1 := +begin + apply integer_dvd (is_integral h hpos) (polynomial.monic.is_primitive + (monic_X_pow_sub_C 1 (ne_of_lt hpos).symm)), + simp only [((is_primitive_root.iff_def μ n).mp h).left, aeval_X_pow, ring_hom.eq_int_cast, + int.cast_one, aeval_one, alg_hom.map_sub, sub_self] +end + +end minimal_polynomial + end is_primitive_root