multichoose_one

Mathlib.RingTheory.Binomial

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

← MathLib Explorer

English

For any k, multichoose 1 k equals 1.

Русский

Для любого k, multichoose 1 k = 1.

LaTeX

$$$multichoose\; 1\; k = 1$$$

Lean4

@[simp]
theorem multichoose_one (k : ℕ) : multichoose (1 : R) k = 1 := by
  induction k with
  | zero => exact multichoose_zero_right 1
  | succ n ih =>
    rw [show (1 : R) = 0 + 1 by exact (@zero_add R _ 1).symm, multichoose_succ_succ, multichoose_zero_succ, zero_add,
      zero_add, ih]

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

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

Разделы

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

Аффилиация

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