descPochhammer_pos — Mathlib

English

In a strictly ordered ring S, if s > n − 1, then the value (descPochhammer S n).eval(s) is strictly positive.

Русский

В строго упорядоченном кольце S при s > n − 1 значение (descPochhammer S n).eval(s) строго положительно.

LaTeX

$$$\\text{If } n \\in \\mathbb{N},\\ s \\in S,\\ h: n - 1 < s,\\text{ then } 0 < (\\operatorname{descPochhammer} \\, S\\, n).\\mathrm{eval}\\, s$.$$

Lean4

/-- `descPochhammer S n` is positive on `(n-1, ∞)`. -/
theorem descPochhammer_pos {n : ℕ} {s : S} (h : n - 1 < s) : 0 < (descPochhammer S n).eval s :=
  by
  rw [← sub_pos, ← sub_add] at h
  rw [descPochhammer_eval_eq_ascPochhammer]
  exact ascPochhammer_pos n (s - n + 1) h

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