cyclotomic_irreducible_of_irreducible_pow

English

If cyclotomic(p^n) is irreducible, then cyclotomic(p^1) is irreducible.

Русский

Если cyclotomic(p^n) ирредуцируем, то cyclotomic(p) ирредуцируем.

LaTeX

$$Irreducible( cyclotomic(p^1) R )$$

Lean4

/-- If `Irreducible (cyclotomic (p ^ n) R)` then `Irreducible (cyclotomic p R).` -/
theorem cyclotomic_irreducible_of_irreducible_pow {p : ℕ} (hp : Nat.Prime p) {R} [CommRing R] [IsDomain 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

Похожие утверждения