multichoose_eq_multichoose — Mathlib

English

Let R be a binomial ring. For every element r in R and every natural number n, the two ways of defining the multichoose operation agree; i.e., BinomialRing.multichoose r n coincides with the standard multichoose function on R.

Русский

Пусть R — биномиальное кольцо. Для любого элемента r в R и любого натурального числа n две реализации операции multichoose совпадают; то есть BinomialRing.multichoose r n совпадает с обычной функцией multichoose на R.

LaTeX

$$$\ BinomialRing.multichoose \; r \; n = multichoose \; r \; n $$$

Lean4

@[simp]
theorem multichoose_eq_multichoose (r : R) (n : ℕ) : BinomialRing.multichoose r n = multichoose r n :=
  rfl

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