cyclotomic_ne_zero — Mathlib

English

The cyclotomic polynomial cyclotomic n R is nonzero for all n in a nontrivial ring R.

Русский

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

LaTeX

$$$\operatorname{cyclotomic}(n,R) \neq 0$$$

Lean4

/-- `cyclotomic n R` is different from `0`. -/
theorem cyclotomic_ne_zero (n : ℕ) (R : Type*) [Ring R] [Nontrivial R] : cyclotomic n R ≠ 0 :=
  (cyclotomic.monic n R).ne_zero

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