choose_eq_fast_choose

Mathlib.Data.Nat.Choose.Basic

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

English

For all n,k, Nat.choose n k equals Nat.fast_choose n k.

Русский

Для всех n,k выполнено: C(n,k) = fast_choose(n,k).

LaTeX

$$$$ \binom{n}{k} = \mathrm{fast\_choose}(n,k) $$$$

Lean4

@[csimp]
theorem choose_eq_fast_choose : Nat.choose = fast_choose :=
  funext (fun _ => funext (Nat.choose_eq_descFactorial_div_factorial _))

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

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

Разделы

Аффилиация

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