English
If p is prime and hmn ≤, then given Irreducible cyclotomic(p^n) one concludes Irreducible cyclotomic(p^m) for smaller exponents.
Русский
Пусть p — простое. Если Irreducible(cyclotomic(p^n)) тогда Irreducible(cyclotomic(p^m)) для меньших степеней.
LaTeX
$$Irreducible(cyclotomic(p^n) R) → Irreducible(cyclotomic(p^m) R) for m ≤ n$$
Lean4
/-- If the `p ^ n`th cyclotomic polynomial is irreducible, so is the `p ^ m`th, for `m ≤ n`. -/
theorem cyclotomic_irreducible_pow_of_irreducible_pow {p : ℕ} (hp : Nat.Prime p) {R} [CommRing R] [IsDomain R] {n m : ℕ}
(hmn : m ≤ n) (h : Irreducible (cyclotomic (p ^ n) R)) : Irreducible (cyclotomic (p ^ m) R) :=
by
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
| zero => simpa using h
| succ k hk =>
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 cutsat) (of_irreducible_expand hp.ne_zero h)
