multichoose_one_right'

Mathlib.RingTheory.Binomial

URI: https://scilib.ai/kg/mathlib#Ring.multichoose_one_right'

← MathLib Explorer

English

For all r in a binomial ring R, multichoose r 1 equals r^1.

Русский

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

LaTeX

$$$multichoose\; r\; 1 = r^1$$$

Lean4

@[simp]
theorem multichoose_one_right' (r : R) : multichoose r 1 = r ^ 1 := by
  rw [← nsmul_right_inj (Nat.factorial_ne_zero 1), factorial_nsmul_multichoose_eq_ascPochhammer, ascPochhammer_one,
    smeval_X, Nat.factorial_one, one_smul]

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

Научная платформа российской исследовательской школы.

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru