Theorems · Theorem · commutative algebra

descPochhammer_pos

∀ {S : Type u_1} [inst : Ring S] [inst_1 : PartialOrder S] [IsStrictOrderedRing S] {n : ℕ} {s : S},
  ↑n - 1 < s → 0 < Polynomial.eval s (descPochhammer S n)

descPochhammer S n is positive on (n-1, ∞).

Defined in

Mathlib.RingTheory.Polynomial.Pochhammer

Cited by

1 results in Mathlib

Foundations

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

Assumes

RingPartialOrderIsStrictOrderedRing