choose_two_right

Mathlib.Data.Nat.Choose.Basic

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

← MathLib Explorer

English

For every natural n, C(n,2) = n(n-1)/2.

Русский

Для любого n ∈ ℕ: C(n,2) = n(n-1)/2.

LaTeX

$$$\\\\binom{n}{2} = \\\\dfrac{n(n-1)}{2}$$$

Lean4

/-- `choose n 2` is the `n`-th triangle number. -/
theorem choose_two_right (n : ℕ) : choose n 2 = n * (n - 1) / 2 := by
  induction n with
  | zero => simp
  | succ n ih =>
    rw [triangle_succ n, choose, ih]
    simp [Nat.add_comm]

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

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

Разделы

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

Аффилиация

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