cast_factorial — Mathlib

English

Let S be a semiring and a a natural number. Then the factorial a! viewed in S equals the value at 1 of the rising factorial ascPochhammer(S,a).

Русский

Пусть S — полукольцо и a ∈ ℕ. Тогда отображение a! в S равно значению восходящего факториала ascPochhammer(S,a) в точке 1.

LaTeX

$$$ (a ! : S) = (ascPochhammer S a).eval 1 $$$

Lean4

theorem cast_factorial : (a ! : S) = (ascPochhammer S a).eval 1 := by
  rw [← one_ascFactorial, cast_ascFactorial, cast_one]

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