choose_symm

Mathlib.Data.Nat.Choose.Basic

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

← MathLib Explorer

English

For all n ≥ k ≥ 0, C(n, n-k) = C(n,k).

Русский

Для всех n ≥ k ≥ 0 выполняется C(n, n-k) = C(n,k).

LaTeX

$$$\\\\binom{n}{n-k} = \\\\binom{n}{k}$$$

Lean4

@[simp]
theorem choose_symm {n k : ℕ} (hk : k ≤ n) : choose n (n - k) = choose n k := by
  rw [choose_eq_factorial_div_factorial hk, choose_eq_factorial_div_factorial (Nat.sub_le _ _), Nat.sub_sub_self hk,
    Nat.mul_comm]

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

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

Разделы

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

Аффилиация

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