binomial_one

Mathlib.Data.Nat.Choose.Multinomial

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

English

For any a and f, multinomial {a} f = 1.

Русский

Для любого a и f: multinomial {a} f = 1.

LaTeX

$$$ \\operatorname{multinomial}(\\{a\\}, f) = 1 $$$

Lean4

theorem binomial_one [DecidableEq α] (h : a ≠ b) (h₁ : f a = 1) : multinomial { a, b } f = (f b).succ := by simp [h, h₁]

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

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

Разделы

Аффилиация

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