irreducible_rat — Mathlib

English

For n > 0, cyclotomic n ℚ is irreducible.

Русский

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

LaTeX

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

Lean4

/-- `cyclotomic n ℚ` is irreducible. -/
theorem irreducible_rat {n : ℕ} (hpos : 0 < n) : Irreducible (cyclotomic n ℚ) :=
  by
  rw [← map_cyclotomic_int]
  exact
    (IsPrimitive.irreducible_iff_irreducible_map_fraction_map (cyclotomic.isPrimitive n ℤ)).1
      (cyclotomic.irreducible hpos)

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