multichoose_two

Mathlib.RingTheory.Binomial

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

← MathLib Explorer

English

For all k, multichoose 2 k equals k + 1.

Русский

Для всех k, multichoose 2 k = k + 1.

LaTeX

$$$multichoose\; 2\; k = k + 1$$$

Lean4

theorem multichoose_two (k : ℕ) : multichoose (2 : R) k = k + 1 := by
  induction k with
  | zero => rw [multichoose_zero_right, Nat.cast_zero, zero_add]
  | succ n ih =>
    rw [one_add_one_eq_two.symm, multichoose_succ_succ, multichoose_one, one_add_one_eq_two, ih, Nat.cast_succ,
      add_comm]

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

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

Разделы

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

Аффилиация

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