feat(polynomial/cyclotomic/basic): ɸ_pⁱ irreducible → ɸ_pʲ irreducibl…

…e for j ≤ i (#13952)

Co-authored-by: Eric Rodriguez <37984851+ericrbg@users.noreply.github.com>

src/number_theory/cyclotomic/discriminant.lean

@@ -66,7 +66,6 @@ lemma discr_prime_pow_ne_two [is_cyclotomic_extension {p ^ (k + 1)} K L] [hp : f
   discr K (hζ.power_basis K).basis =
   (-1) ^ (((p ^ (k + 1) : ℕ).totient) / 2) * p ^ ((p : ℕ) ^ k * ((p - 1) * (k + 1) - 1)) :=
 begin
-  have hirr₁ := cyclotomic_irreducible_of_irreducible_pow hp.1 k.succ_ne_zero hirr,
   haveI : ne_zero ((↑(p ^ (k + 1)) : ℕ) : K),
   { refine ⟨λ hzero, _⟩,
     rw [pnat.pow_coe] at hzero,
@@ -116,8 +115,8 @@ begin
     replace H := congr_arg (algebra.norm K) H,
     have hnorm : (norm K) (ζ ^ (p : ℕ) ^ k - 1) = p ^ ((p : ℕ) ^ k),
     { by_cases hp : p = 2,
-      { exact hζ.pow_sub_one_norm_prime_pow_of_one_le hirr (by simpa using hirr₁) rfl.le (hp2 hp) },
-      { exact hζ.pow_sub_one_norm_prime_ne_two hirr (by simpa using hirr₁) rfl.le hp } },
+      { exact hζ.pow_sub_one_norm_prime_pow_of_one_le hirr rfl.le (hp2 hp) },
+      { exact hζ.pow_sub_one_norm_prime_ne_two hirr rfl.le hp } },
     rw [monoid_hom.map_mul, hnorm, monoid_hom.map_mul, ← map_nat_cast (algebra_map K L),
       algebra.norm_algebra_map, finrank _ hirr, pnat.pow_coe, totient_prime_pow hp.out (succ_pos k),
       nat.sub_one, nat.pred_succ, ← hζ.minpoly_eq_cyclotomic_of_irreducible hirr, map_pow,

src/number_theory/cyclotomic/primitive_roots.lean

@@ -37,11 +37,10 @@ in the implementation details section.
 * `is_primitive_root.sub_one_norm_eq_eval_cyclotomic`: if `irreducible (cyclotomic n K)`
   (in particular for `K = ℚ`), then the norm of `ζ - 1` is `eval 1 (cyclotomic n ℤ)`, for a
   primitive root ζ. We also prove the analogous of this result for `zeta`.
-* `is_primitive_root.pow_prime_pow_sub_one_norm` : if
-  `irreducible (cyclotomic (p ^ (k + 1)) K)` and `irreducible (cyclotomic (p ^ (k - s + 1)) K))`
-  (in particular for `K = ℚ`) and `p` is a prime, then the norm of `ζ ^ (p ^ s) - 1` is
-  `p ^ (p ^ s)` `p ^ (k - s + 1) ≠ 2`. See the following lemmas for similar results. We  also prove
-  the analogous of this result for `zeta`.
+* `is_primitive_root.pow_sub_one_norm_prime_pow_ne_two` : if
+  `irreducible (cyclotomic (p ^ (k + 1)) K)` (in particular for `K = ℚ`) and `p` is a prime,
+  then the norm of `ζ ^ (p ^ s) - 1` is `p ^ (p ^ s)` `p ^ (k - s + 1) ≠ 2`. See the following
+  lemmas for similar results. We also prove the analogous of this result for `zeta`.
 * `is_primitive_root.sub_one_norm_prime_ne_two` : if `irreducible (cyclotomic (p ^ (k + 1)) K)`
   (in particular for `K = ℚ`) and `p` is an odd prime, then the norm of `ζ - 1` is `p`. We also
   prove the analogous of this result for `zeta`.
@@ -285,15 +284,13 @@ omit hζ
 local attribute [instance] is_cyclotomic_extension.finite_dimensional
 local attribute [instance] is_cyclotomic_extension.is_galois
 
-/-- If `irreducible (cyclotomic (p ^ (k + 1)) K)` and
-`irreducible (cyclotomic (p ^ (k - s + 1)) K))` (in particular for `K = ℚ`) and `p` is a prime,
+/-- If `irreducible (cyclotomic (p ^ (k + 1)) K)` (in particular for `K = ℚ`) and `p` is a prime,
 then the norm of `ζ ^ (p ^ s) - 1` is `p ^ (p ^ s)` if `p ^ (k - s + 1) ≠ 2`. See the next lemmas
 for similar results. -/
 lemma pow_sub_one_norm_prime_pow_ne_two [ne_zero ((p : ℕ) : K)] {k s : ℕ}
   (hζ : is_primitive_root ζ ↑(p ^ (k + 1))) [hpri : fact (p : ℕ).prime]
   [is_cyclotomic_extension {p ^ (k + 1)} K L]
-  (hirr : irreducible (cyclotomic (↑(p ^ (k + 1)) : ℕ) K))
-  (hirr₁ : irreducible (cyclotomic (↑(p ^ (k - s + 1)) : ℕ) K)) (hs : s ≤ k)
+  (hirr : irreducible (cyclotomic (↑(p ^ (k + 1)) : ℕ) K)) (hs : s ≤ k)
   (htwo : p ^ (k - s + 1) ≠ 2) : norm K (ζ ^ ((p : ℕ) ^ s) - 1) = p ^ ((p : ℕ) ^ s) :=
 begin
   haveI : ne_zero ((↑(p ^ (k + 1)) : ℕ) : K),
@@ -305,6 +302,9 @@ begin
     rw [pnat.pow_coe] at hzero,
     simpa [ne_zero.ne ((p : ℕ) : K)] using hzero },
 
+  have hirr₁ : irreducible (cyclotomic (p ^ (k - s + 1)) K) :=
+  cyclotomic_irreducible_pow_of_irreducible_pow hpri.1 (by linarith) hirr,
+  rw ←pnat.pow_coe at hirr₁,
   let η := ζ ^ ((p : ℕ) ^ s) - 1,
   let η₁ : K⟮η⟯ := intermediate_field.adjoin_simple.gen K η,
   have hη : is_primitive_root (η + 1) (p ^ (k + 1 - s)),
@@ -354,17 +354,15 @@ begin
   all_goals { apply_instance }
 end
 
-/-- If `irreducible (cyclotomic (p ^ (k + 1)) K)` and
-`irreducible (cyclotomic (p ^ (k - s + 1)) K))` (in particular for `K = ℚ`) and `p` is a prime,
+/-- If `irreducible (cyclotomic (p ^ (k + 1)) K)` (in particular for `K = ℚ`) and `p` is a prime,
 then the norm of `ζ ^ (p ^ s) - 1` is `p ^ (p ^ s)` if `p ≠ 2`. -/
 lemma pow_sub_one_norm_prime_ne_two [ne_zero ((p : ℕ) : K)] {k : ℕ}
   (hζ : is_primitive_root ζ ↑(p ^ (k + 1))) [hpri : fact (p : ℕ).prime]
   [is_cyclotomic_extension {p ^ (k + 1)} K L]
-  (hirr : irreducible (cyclotomic (↑(p ^ (k + 1)) : ℕ) K))  {s : ℕ}
-  (hirr₁ : irreducible (cyclotomic (↑(p ^ (k - s + 1)) : ℕ) K)) (hs : s ≤ k)
+  (hirr : irreducible (cyclotomic (↑(p ^ (k + 1)) : ℕ) K)) {s : ℕ} (hs : s ≤ k)
   (hodd : p ≠ 2) : norm K (ζ ^ ((p : ℕ) ^ s) - 1) = p ^ ((p : ℕ) ^ s) :=
 begin
-  refine hζ.pow_sub_one_norm_prime_pow_ne_two hirr hirr₁ hs (λ h, _),
+  refine hζ.pow_sub_one_norm_prime_pow_ne_two hirr hs (λ h, _),
   rw [← pnat.coe_inj, pnat.coe_bit0, pnat.one_coe, pnat.pow_coe, ← pow_one 2] at h,
   replace h := eq_of_prime_pow_eq (prime_iff.1 hpri.out) (prime_iff.1 nat.prime_two)
     ((k - s).succ_pos) h,
@@ -379,7 +377,7 @@ lemma sub_one_norm_prime_ne_two [ne_zero ((p : ℕ) : K)] {k : ℕ}
   [is_cyclotomic_extension {p ^ (k + 1)} K L]
   (hirr : irreducible (cyclotomic (↑(p ^ (k + 1)) : ℕ) K)) (h : p ≠ 2) :
   norm K (ζ - 1) = p :=
-by simpa using hζ.pow_sub_one_norm_prime_ne_two hirr (by exact hirr) (zero_le k) h
+by simpa using hζ.pow_sub_one_norm_prime_ne_two hirr k.zero_le h
 
 /-- If `irreducible (cyclotomic p K)` (in particular for `K = ℚ`) and `p` is an odd prime,
 then the norm of `ζ - 1` is `p`. -/
@@ -441,14 +439,12 @@ begin
   simpa [hk₁] using sub_one_norm_eq_eval_cyclotomic hζ this hirr,
 end
 
-/-- If `irreducible (cyclotomic (p ^ (k + 1)) K)` and
-`irreducible (cyclotomic (p ^ (k - s + 1)) K))` (in particular for `K = ℚ`) and `p` is a prime,
+/-- If `irreducible (cyclotomic (p ^ (k + 1)) K)` (in particular for `K = ℚ`) and `p` is a prime,
 then the norm of `ζ ^ (p ^ s) - 1` is `p ^ (p ^ s)` if `1 ≤ k`. -/
 lemma pow_sub_one_norm_prime_pow_of_one_le [hne : ne_zero ((p : ℕ) : K)] {k s : ℕ}
   (hζ : is_primitive_root ζ ↑(p ^ (k + 1))) [hpri : fact (p : ℕ).prime]
   [hcycl : is_cyclotomic_extension {p ^ (k + 1)} K L]
-  (hirr : irreducible (cyclotomic (↑(p ^ (k + 1)) : ℕ) K))
-  (hirr₁ : irreducible (cyclotomic (↑(p ^ (k - s + 1)) : ℕ) K)) (hs : s ≤ k)
+  (hirr : irreducible (cyclotomic (↑(p ^ (k + 1)) : ℕ) K)) (hs : s ≤ k)
   (hk : 1 ≤ k) : norm K (ζ ^ ((p : ℕ) ^ s) - 1) = p ^ ((p : ℕ) ^ s) :=
 begin
   by_cases htwo : p ^ (k - s + 1) = 2,
@@ -474,7 +470,7 @@ begin
     rw [hζ.pow_sub_one_norm_two hirr],
     rw [hk₁, pow_succ, pow_mul, neg_eq_neg_one_mul, mul_pow, neg_one_sq, one_mul, ← pow_mul,
       ← pow_succ] },
-  { exact hζ.pow_sub_one_norm_prime_pow_ne_two hirr hirr₁ hs htwo }
+  { exact hζ.pow_sub_one_norm_prime_pow_ne_two hirr hs htwo }
 end
 
 end is_primitive_root
@@ -505,14 +501,13 @@ begin
   exact (zeta_primitive_root n K L).sub_one_norm_is_prime_pow hn hirr h,
 end
 
-/-- If `irreducible (cyclotomic (p ^ (k + 1)) K)` and `irreducible (cyclotomic (p ^ (k - s + 1)) K)`
-(in particular for `K = ℚ`) and `p` is a prime, then the norm of
-`(zeta (p ^ (k + 1)) K L) ^ (p ^ s) - 1` is `p ^ (p ^ s)` if `p ^ (k - s + 1) ≠ 2`. -/
+/-- If `irreducible (cyclotomic (p ^ (k + 1)) K)` (in particular for `K = ℚ`) and `p` is a prime,
+then the norm of `(zeta (p ^ (k + 1)) K L) ^ (p ^ s) - 1` is `p ^ (p ^ s)`
+if `p ^ (k - s + 1) ≠ 2`. -/
 lemma prime_ne_two_pow_norm_zeta_pow_sub_one [ne_zero ((p : ℕ) : K)] {k : ℕ}
   [hpri : fact (p : ℕ).prime]
   [is_cyclotomic_extension {p ^ (k + 1)} K L]
-  (hirr : irreducible (cyclotomic (↑(p ^ (k + 1)) : ℕ) K))  {s : ℕ}
-  (hirr₁ : irreducible (cyclotomic (↑(p ^ (k - s + 1)) : ℕ) K)) (hs : s ≤ k)
+  (hirr : irreducible (cyclotomic (↑(p ^ (k + 1)) : ℕ) K))  {s : ℕ} (hs : s ≤ k)
   (htwo : p ^ (k - s + 1) ≠ 2) :
   norm K ((zeta (p ^ (k + 1)) K L) ^ ((p : ℕ) ^ s) - 1) = p ^ ((p : ℕ) ^ s) :=
 begin
@@ -521,7 +516,7 @@ begin
   { refine ⟨λ hzero, _⟩,
     rw [pow_coe] at hzero,
     simpa [ne_zero.ne ((p : ℕ) : L)] using hzero },
-  exact (zeta_primitive_root _ K L).pow_sub_one_norm_prime_pow_ne_two hirr hirr₁ hs htwo
+  exact (zeta_primitive_root _ K L).pow_sub_one_norm_prime_pow_ne_two hirr hs htwo
 end
 
 /-- If `irreducible (cyclotomic (p ^ (k + 1)) K)` (in particular for `K = ℚ`) and `p` is an odd

src/ring_theory/polynomial/cyclotomic/basic.lean

@@ -956,20 +956,28 @@ begin
         nat.totient_mul_of_prime_of_dvd hp hdiv, mul_comm] }
 end
 
-/-- If `irreducible (cyclotomic (p ^ n) R)` then `irreducible (cyclotomic p R).` -/
---TODO: add `irreducible (cyclotomic (p ^ m) R)` if `m ≤ n`.
-lemma cyclotomic_irreducible_of_irreducible_pow {p : ℕ} (hp : nat.prime p)
-  {R} [comm_ring R] [is_domain R] :
-  ∀ {n : ℕ}, n ≠ 0 → irreducible (cyclotomic (p ^ n) R) → irreducible (cyclotomic p R)
-| 0     hn _ := by contradiction
-| 1     hn h := by rwa pow_one at h
-| (n+2) hn h :=
+/-- If the `p ^ n`th cyclotomic polynomial is irreducible, so is the `p ^ m`th, for `m ≤ n`. -/
+lemma cyclotomic_irreducible_pow_of_irreducible_pow {p : ℕ} (hp : nat.prime p)
+  {R} [comm_ring R] [is_domain R] {n m : ℕ} (hmn : m ≤ n)
+  (h : irreducible (cyclotomic (p ^ n) R)) : irreducible (cyclotomic (p ^ m) R) :=
 begin
-  rw [pow_succ', ←cyclotomic_expand_eq_cyclotomic hp $ dvd_pow_self p n.succ_ne_zero] at h,
-  replace h := of_irreducible_expand hp.ne_zero h,
-  refine cyclotomic_irreducible_of_irreducible_pow n.succ_ne_zero h
+  unfreezingI
+  { rcases m.eq_zero_or_pos with rfl | hm,
+    { simpa using irreducible_X_sub_C (1 : R) },
+    obtain ⟨k, rfl⟩ := nat.exists_eq_add_of_le hmn,
+    induction k with k hk },
+  { simpa using h },
+  have : m + k ≠ 0 := (add_pos_of_pos_of_nonneg hm k.zero_le).ne',
+  rw [nat.add_succ, pow_succ', ←cyclotomic_expand_eq_cyclotomic hp $ dvd_pow_self p this] at h,
+  exact hk (by linarith) (of_irreducible_expand hp.ne_zero h)
 end
 
+/-- If `irreducible (cyclotomic (p ^ n) R)` then `irreducible (cyclotomic p R).` -/
+lemma cyclotomic_irreducible_of_irreducible_pow {p : ℕ} (hp : nat.prime p) {R} [comm_ring R]
+  [is_domain R] {n : ℕ} (hn : n ≠ 0) (h : irreducible (cyclotomic (p ^ n) R)) :
+  irreducible (cyclotomic p R) :=
+pow_one p ▸ cyclotomic_irreducible_pow_of_irreducible_pow hp hn.bot_lt h
+
 end expand
 
 section char_p