irreducible — Mathlib

English

For n > 0, the cyclotomic n ℤ is irreducible.

Русский

Для n > 0 циклотоми́ческий n ℤ неразложим.

LaTeX

$$$$ \\operatorname{irreducible}(\\operatorname{cyclotomic}(n, \\mathbb{Z})). $$$$

Lean4

/-- `cyclotomic n ℤ` is irreducible. -/
theorem irreducible {n : ℕ} (hpos : 0 < n) : Irreducible (cyclotomic n ℤ) :=
  by
  rw [cyclotomic_eq_minpoly (isPrimitiveRoot_exp n hpos.ne') hpos]
  apply minpoly.irreducible
  exact (isPrimitiveRoot_exp n hpos.ne').isIntegral hpos

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