degree_cyclotomic_pos — Mathlib

English

If n > 0, then the degree of the cyclotomic polynomial Φ_n over a ring R is positive.

Русский

Если n > 0, то deg Φ_n над кольцом R положительна.

LaTeX

$$$$0 < \deg(\mathrm{cyclotomic} \ n \ R) \quad\text{for}\quad 0 < n.$$$$

Lean4

/-- The degree of `cyclotomic n R` is positive. -/
theorem degree_cyclotomic_pos (n : ℕ) (R : Type*) (hpos : 0 < n) [Ring R] [Nontrivial R] :
    0 < (cyclotomic n R).degree := by rwa [degree_cyclotomic n R, Nat.cast_pos, Nat.totient_pos]

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