English
There is a canonical BinomialRing structure on the integers, with multichoose and factorial_nsmul_multichoose aligning with the smeval of ascPochhammer and the factorial-descent relations.
Русский
На множествах целых чисел существует каноническая структура BinomialRing, для которой multichoose и factorial_nsmul_multichoose согласованы с smeval ascPochhammer и соотношениями факториалов.
LaTeX
$$$\text{BinomialRing } \mathbb{Z}$ with multichoose, factorial_nsmul_multichoose$$$
Lean4
instance instBinomialRing : BinomialRing ℤ
where
multichoose := Int.multichoose
factorial_nsmul_multichoose r
k := by
rw [Int.multichoose.eq_def, nsmul_eq_mul]
cases r with
| ofNat n =>
simp only [Int.ofNat_eq_coe, Int.ofNat_mul_out]
rw [← Nat.descFactorial_eq_factorial_mul_choose, smeval_at_natCast, ← eval_eq_smeval n,
ascPochhammer_nat_eq_descFactorial]
| negSucc n =>
simp only
rw [mul_comm, mul_assoc, ← Nat.cast_mul, mul_comm _ (k.factorial), ← Nat.descFactorial_eq_factorial_mul_choose, ←
descPochhammer_smeval_eq_descFactorial, ← Int.neg_ofNat_succ, ascPochhammer_smeval_neg_eq_descPochhammer]
norm_cast
-- This instance will fire for any type `R`, so is local unless needed elsewhere.
