cyclotomic_pos' — Mathlib

English

For any n in an ordered ring, if 1 < x then 0 < eval x cyclotomic n R.

Русский

Для любого n в упорядоченном кольце, если 1 < x, то 0 < eval x cyclotomic n R.

LaTeX

$$0 < eval(x, cyclotomic(n, R)) for 1 < x$$

Lean4

/-- Cyclotomic polynomials are always positive on inputs larger than one.
Similar to `cyclotomic_pos` but with the condition on the input rather than index of the
cyclotomic polynomial. -/
theorem cyclotomic_pos' (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).1 hx

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