cast_ascFactorial — Mathlib

English

For a semiring S, a,b ∈ Nat, a.ascFactorial b equals the evaluation of the ascPochhammer S b at a cast to S.

Русский

Для полупредела S, a.ascFactorial b равно вычислению ascPochhammer S b в элементе S, полученном из a.

LaTeX

$$a.ascFactorial b = (ascPochhammer S b).eval (a : S)$$

Lean4

theorem cast_ascFactorial : a.ascFactorial b = (ascPochhammer S b).eval (a : S) := by
  rw [← ascPochhammer_nat_eq_ascFactorial, ascPochhammer_eval_cast]

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