multichoose_zero_right' — Mathlib

English

For any r in a binomial ring R, multichoose r 0 equals r^0, i.e., 1.

Русский

Для любого r из биномиального кольца R верно multichoose r 0 = r^0, то есть 1.

LaTeX

$$$multichoose\; r\; 0 = r^0$$$

Lean4

@[simp]
theorem multichoose_zero_right' (r : R) : multichoose r 0 = r ^ 0 := by
  rw [← nsmul_right_inj (Nat.factorial_ne_zero 0), factorial_nsmul_multichoose_eq_ascPochhammer, ascPochhammer_zero,
    smeval_one, Nat.factorial]

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