cast_add_choose

Mathlib.Data.Nat.Choose.Cast

URI: https://scilib.ai/kg/mathlib#Nat.cast_add_choose

← MathLib Explorer

English

For a,b ∈ ℕ, C(a+b,a) = (a+b)!/(a! b!).

Русский

Для любых a,b ∈ ℕ выполняется C(a+b,a) = (a+b)!/(a! b!).

LaTeX

$$$$ \\binom{a+b}{a} = \\frac{(a+b)!}{a!\\,b!}. $$$$

Lean4

theorem cast_add_choose {a b : ℕ} : ((a + b).choose a : K) = (a + b)! / (a ! * b !) := by
  rw [cast_choose K (_root_.le_add_right le_rfl), add_tsub_cancel_left]

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

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

Разделы

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

Аффилиация

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