English
Two internal properties ensuring binomial coefficient operations stay within ℤ_p and behave well under evaluation and factorial manipulations.
Русский
Две внутренние свойности, обеспечивающие, что биномиальные коэффициенты остаются внутри ℤ_p и ведут себя корректно при вычислениях и факториалах.
LaTeX
$$$\text{BinomialRing}(\mathbb{Z}_p)$ and related lemmas regarding multinomial/factorial identities hold in ℤ_p.$$
Lean4
/-- The p-adic integers are a binomial ring, i.e. a ring where binomial coefficients make sense. -/
noncomputable instance instBinomialRing : BinomialRing ℤ_[p] where
-- We define `multichoose` as a fraction in `ℚ_[p]` together with a proof that its norm is `≤ 1`.
multichoose x
k :=
⟨(ascPochhammer ℤ_[p] k).eval x / (k.factorial : ℚ_[p]),
by
rw [norm_div, div_le_one (by simpa using k.factorial_ne_zero)]
exact x.norm_ascPochhammer_le k⟩
factorial_nsmul_multichoose x
k := by
rw [← Subtype.coe_inj, nsmul_eq_mul, PadicInt.coe_mul, PadicInt.coe_natCast,
mul_div_cancel₀ _ (mod_cast k.factorial_ne_zero), Subtype.coe_inj, Polynomial.eval_eq_smeval,
Polynomial.ascPochhammer_smeval_cast]
