choose_one_right'

Mathlib.RingTheory.Binomial

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

English

The binomial coefficient choose r 1 equals r^1.

Русский

Биномный коэффициент choose r 1 равен r^1.

LaTeX

$$$ \forall R\ [NonAssocRing\ R]\ [Pow\ R\ Nat]\ [BinomialRing\ R],\ choose r 1 = r^1$$$

Lean4

@[simp]
theorem choose_one_right' (r : R) : choose r 1 = r ^ 1 := by
  rw [choose, Nat.cast_one, sub_add_cancel, multichoose_one_right']

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

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

Разделы

Аффилиация

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