cyclotomic_nonneg — Mathlib

English

For n and x with x ≥ 1 in a ordered ring, eval x cyclotomic n R ≥ 0.

Русский

Для n и x с x ≥ 1 в упорядоченном кольце eval x cyclotomic n R ≥ 0.

LaTeX

$$0 ≤ eval x (cyclotomic n R)$$

Lean4

/-- Cyclotomic polynomials are always nonnegative on inputs one or more. -/
theorem cyclotomic_nonneg (n : ℕ) {R} [CommRing R] [LinearOrder R] [IsStrictOrderedRing R] {x : R} (hx : 1 ≤ x) :
    0 ≤ eval x (cyclotomic n R) :=
  (cyclotomic_pos_and_nonneg n x).2 hx

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