instBinomialRingOfModuleNNRat — Mathlib

English

There is a noncomputable construction providing a BinomialRing structure on any R which is an NN Rat-module, enabling smeval compatibilities with ascPochhammer.

Русский

Существует неконструктивное построение биномиального кольца на любом модуле NN Rat, которое обеспечивает совместимость smeval с ascPochhammer.

LaTeX

$$$\text{BinomialRing } R$ given $R$-NNRat module$$

Lean4

noncomputable instance {R : Type*} [AddCommMonoid R] [Module ℚ≥0 R] [Pow R ℕ] : BinomialRing R
    where
  multichoose r n := (n.factorial : ℚ≥0)⁻¹ • Polynomial.smeval (ascPochhammer ℕ n) r
  factorial_nsmul_multichoose r
    n := by
    match_scalars
    field_simp

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