multinomial_zero

Mathlib.Data.Nat.Choose.Multinomial

URI: https://scilib.ai/kg/mathlib#Multiset.multinomial_zero

English

The multinomial of the empty multiset is 1.

Русский

Мультиномиал пустого мультимножества равен 1.

LaTeX

$$[simp] multinomial (0 : Multiset α) = 1$$

Lean4

@[simp]
theorem multinomial_zero [DecidableEq α] : multinomial (0 : Multiset α) = 1 := by
  simp [multinomial, Finsupp.multinomial]

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

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

Разделы

Аффилиация

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