English
Natural numbers carry a canonical binomial ring structure, where multichoose and ascPochhammer are compatible with the usual combinatorial interpretations.
Русский
Естественные числа имеют каноническую структуру биномиального кольца, в которой multichoose и ascPochhammer согласованы с обычной комбинаторной интерпретацией.
LaTeX
$$$\text{BinomialRing}\; \mathbb{N}\;\text{(multichoose, ascPochhammer)}$$$
Lean4
instance instBinomialRing : BinomialRing ℕ
where
multichoose := Nat.multichoose
factorial_nsmul_multichoose r
n := by
rw [smul_eq_mul, Nat.multichoose_eq r n, ← Nat.descFactorial_eq_factorial_mul_choose, ←
eval_eq_smeval r (ascPochhammer ℕ n), ascPochhammer_nat_eq_descFactorial]
