cast_choose_two

Mathlib.Data.Nat.Choose.Cast

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

← MathLib Explorer

English

For any a ∈ ℕ, C(a,2) = a(a−1)/2.

Русский

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

LaTeX

$$$$ \\binom{a}{2} = \\frac{a(a-1)}{2}. $$$$

Lean4

theorem cast_choose_two (a : ℕ) : (a.choose 2 : K) = a * (a - 1) / 2 := by
  rw [← cast_descFactorial_two, descFactorial_eq_factorial_mul_choose, factorial_two, mul_comm, cast_mul, cast_two,
    eq_div_iff_mul_eq (two_ne_zero : (2 : K) ≠ 0)]

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

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

Разделы

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

Аффилиация

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