From 7bc2e9efa504fd256b1fc033adee602e8264596a Mon Sep 17 00:00:00 2001
From: Riccardo Brasca <riccardo.brasca@gmail.com>
Date: Thu, 7 Jan 2021 13:09:25 +0000
Subject: [PATCH] feat(ring_theory/polynomial/cyclotomic): add
 cyclotomic.irreducible (#5642)

I proved irreducibility of cyclotomic polynomials, showing that `cyclotomic n Z` is the minimal polynomial of any primitive root of unity.
---
 src/data/polynomial/ring_division.lean     | 23 ++++++++++
 src/ring_theory/polynomial/cyclotomic.lean | 49 +++++++++++++++++++++-
 src/ring_theory/roots_of_unity.lean        |  1 -
 3 files changed, 70 insertions(+), 3 deletions(-)

diff --git a/src/data/polynomial/ring_division.lean b/src/data/polynomial/ring_division.lean
index 5e994731a2428..10676ed147e90 100644
--- a/src/data/polynomial/ring_division.lean
+++ b/src/data/polynomial/ring_division.lean
@@ -538,6 +538,29 @@ begin
   exact hrew.symm
 end
 
+lemma eq_of_monic_of_dvd_of_nat_degree_le (hp : p.monic) (hq : q.monic) (hdiv : p ∣ q)
+  (hdeg : q.nat_degree ≤ p.nat_degree) : q = p :=
+begin
+  obtain ⟨r, hr⟩ := hdiv,
+  have rzero : r ≠ 0,
+  { intro h,
+    simpa [h, monic.ne_zero hq] using hr },
+  rw [hr, nat_degree_mul (monic.ne_zero hp) rzero] at hdeg,
+  have hdegeq : p.nat_degree + r.nat_degree = p.nat_degree,
+  { suffices hdegle : p.nat_degree ≤ p.nat_degree + r.nat_degree,
+    { exact le_antisymm hdeg hdegle },
+    exact nat.le.intro rfl },
+  replace hdegeq := eq_C_of_nat_degree_eq_zero (((@add_right_inj _ _ p.nat_degree) _ 0).1 hdegeq),
+  suffices hlead : 1 = r.leading_coeff,
+  { have hcoeff := leading_coeff_C (r.coeff 0),
+    rw [← hdegeq, ← hlead] at hcoeff,
+    rw [← hcoeff, C_1] at hdegeq,
+    rwa [hdegeq, mul_one] at hr },
+  have hprod : q.leading_coeff = p.leading_coeff * r.leading_coeff,
+  { simp only [hr, leading_coeff_mul] },
+  rwa [monic.leading_coeff hp, monic.leading_coeff hq, one_mul] at hprod
+end
+
 end integral_domain
 
 section
diff --git a/src/ring_theory/polynomial/cyclotomic.lean b/src/ring_theory/polynomial/cyclotomic.lean
index 3a488311b979d..8378d4d011563 100644
--- a/src/ring_theory/polynomial/cyclotomic.lean
+++ b/src/ring_theory/polynomial/cyclotomic.lean
@@ -33,17 +33,20 @@ comes from a polynomial with integer coefficients.
 * `prod_cyclotomic_eq_X_pow_sub_one` : `X ^ n - 1 = ∏ (cyclotomic i)`, where `i` divides `n`.
 * `cyclotomic_eq_prod_X_pow_sub_one_pow_moebius` : The Möbius inversion formula for
   `cyclotomic n R` over an abstract fraction field for `polynomial R`.
+* `cyclotomic.irreducible` : `cyclotomic n ℤ` is irreducible.
 
 ## Implementation details
 
 Our definition of `cyclotomic' n R` makes sense in any integral domain `R`, but the interesting
-results hold if there is a primitive `n`th root of unity in `R`. In particular, our definition is
+results hold if there is a primitive `n`-th root of unity in `R`. In particular, our definition is
 not the standard one unless there is a primitive `n`th root of unity in `R`. For example,
 `cyclotomic' 3 ℤ = 1`, since there are no primitive cube roots of unity in `ℤ`. The main example is
 `R = ℂ`, we decided to work in general since the difficulties are essentially the same.
 To get the standard cyclotomic polynomials, we use `int_coeff_of_cycl`, with `R = ℂ`, to get a
 polynomial with integer coefficients and then we map it to `polynomial R`, for any ring `R`.
-
+To prove `cyclotomic.irreducible`, the irreducibility of `cyclotomic n ℤ`, we show in
+`minimal_polynomial_primitive_root_eq_cyclotomic` that `cyclotomic n ℤ` is the minimal polynomial of
+any `n`-th primitive root of unity `μ : K`, where `K` is a field of characteristic `0`.
 -/
 
 open_locale classical big_operators
@@ -497,6 +500,15 @@ begin
   cyclotomic'_eq_X_pow_sub_one_div hpos hz, finset.prod_congr (refl k.proper_divisors) h]
 end
 
+/-- Any `n`-th primitive root of unity is a root of `cyclotomic n ℤ`.-/
+lemma is_root_cyclotomic {n : ℕ} {K : Type*} [field K] (hpos : 0 < n) {μ : K}
+  (h : is_primitive_root μ n) : is_root (cyclotomic n K) μ :=
+begin
+  rw [← mem_roots (cyclotomic_ne_zero n K),
+  cyclotomic_eq_prod_X_sub_primitive_roots h, roots_prod_X_sub_C, ← finset.mem_def],
+  rwa [← mem_primitive_roots hpos] at h,
+end
+
 lemma eq_cyclotomic_iff {R : Type*} [comm_ring R] [nontrivial R] {n : ℕ} (hpos: 0 < n)
   (P : polynomial R) :
   P = cyclotomic n R ↔ P * (∏ i in nat.proper_divisors n, polynomial.cyclotomic i R) = X ^ n - 1 :=
@@ -647,3 +659,36 @@ end
 end order
 
 end polynomial
+
+section minimial_polynomial
+
+open is_primitive_root polynomial complex
+
+/-- The minimal polynomial of a primitive `n`-th root of unity `μ` divides `cyclotomic n ℤ`. -/
+lemma minimal_polynomial_primitive_root_dvd_cyclotomic {n : ℕ} {K : Type*} [field K] {μ : K}
+  (h : is_primitive_root μ n) (hpos : 0 < n) [char_zero K] :
+  minimal_polynomial (is_integral h hpos) ∣ cyclotomic n ℤ :=
+begin
+  apply minimal_polynomial.integer_dvd (is_integral h hpos) (cyclotomic.monic n ℤ).is_primitive,
+  simpa [aeval_def, eval₂_eq_eval_map, is_root.def] using is_root_cyclotomic hpos h
+end
+
+/-- `cyclotomic n ℤ` is the minimal polynomial of a primitive `n`-th root of unity `μ`. -/
+lemma minimal_polynomial_primitive_root_eq_cyclotomic {n : ℕ} {K : Type*} [field K] {μ : K}
+  (h : is_primitive_root μ n) (hpos : 0 < n) [char_zero K] :
+  cyclotomic n ℤ = minimal_polynomial (is_integral h hpos) :=
+begin
+  refine eq_of_monic_of_dvd_of_nat_degree_le (minimal_polynomial.monic (is_integral h hpos))
+    (cyclotomic.monic n ℤ) (minimal_polynomial_primitive_root_dvd_cyclotomic h hpos) _,
+  simpa [nat_degree_cyclotomic n ℤ] using totient_le_degree_minimal_polynomial h hpos
+end
+
+/-- `cyclotomic n ℤ` is irreducible. -/
+lemma cyclotomic.irreducible {n : ℕ} (hpos : 0 < n) : irreducible (cyclotomic n ℤ) :=
+begin
+  have h0 := (ne_of_lt hpos).symm,
+  rw [minimal_polynomial_primitive_root_eq_cyclotomic (is_primitive_root_exp n h0) hpos],
+  exact minimal_polynomial.irreducible (is_integral (is_primitive_root_exp n h0) hpos)
+end
+
+end minimial_polynomial
diff --git a/src/ring_theory/roots_of_unity.lean b/src/ring_theory/roots_of_unity.lean
index b7a0a680ad151..bb19389cee9d7 100644
--- a/src/ring_theory/roots_of_unity.lean
+++ b/src/ring_theory/roots_of_unity.lean
@@ -912,7 +912,6 @@ end
 /-- The degree of the minimal polynomial of `μ` is at least `totient n`. -/
 lemma totient_le_degree_minimal_polynomial : nat.totient n ≤ (minimal_polynomial
   (is_integral h hpos)).nat_degree :=
-
 let P : polynomial ℤ := minimal_polynomial (is_integral h hpos),-- minimal polynomial of `μ`
     P_K : polynomial K := map (int.cast_ring_hom K) P -- minimal polynomial of `μ` sent to `K[X]`
 in calc