monic — Mathlib

English

For every natural number n and every commutative domain R, the polynomial cyclotomic' n R is monic.

Русский

Для любого натурального числа n и любой областьной кольцевой области R полином cyclotomic' n R является моничным.

LaTeX

$$$\operatorname{Monic}(\operatorname{cyclotomic}'(n,R))$$$

Lean4

/-- `cyclotomic' n R` is monic. -/
theorem monic (n : ℕ) (R : Type*) [CommRing R] [IsDomain R] : (cyclotomic' n R).Monic :=
  monic_prod_of_monic _ _ fun _ _ => monic_X_sub_C _

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