Theorems · Theorem · number theory

Polynomial.cyclotomic_pos

∀ {n : ℕ},
  2 < n →
    ∀ {R : Type u_1} [inst : CommRing R] [inst_1 : LinearOrder R] [IsStrictOrderedRing R] (x : R),
      0 < Polynomial.eval x (Polynomial.cyclotomic n R)

Defined in

Mathlib.RingTheory.Polynomial.Cyclotomic.Eval

Cited by

1 results in Mathlib

Foundations

Depth 210 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

CommRingLinearOrderIsStrictOrderedRing