multichoose_one_right

Mathlib.RingTheory.Binomial

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

English

In a binomial ring, multichoose r 1 coincides with r; i.e., multichoose r 1 = r.

Русский

В биномиальном кольце multichoose r 1 совпадает с r; то есть multichoose r 1 = r.

LaTeX

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

Lean4

theorem multichoose_one_right [MulOneClass R] [NatPowAssoc R] (r : R) : multichoose r 1 = r := by
  rw [multichoose_one_right', npow_one]

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

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

Разделы

Аффилиация

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