count_ofSums_zero

Mathlib.Combinatorics.Enumerative.Partition

URI: https://scilib.ai/kg/mathlib#Nat.Partition.count_ofSums_zero

English

If hl: l.sum = n, then the number of zeros in the parts of ofSums is zero.

Русский

Если hl: l.sum = n, то число нулей в частях ofSums равно нулю.

LaTeX

$$$\operatorname{Multiset.count}(0, (\mathrm{ofSums}(n,l,hl).\mathrm{parts})) = 0$$$

Lean4

theorem count_ofSums_zero {n : ℕ} {l : Multiset ℕ} (hl : l.sum = n) : (ofSums n l hl).parts.count 0 = 0 :=
  count_filter_of_neg fun h => h rfl

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

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

Разделы

Аффилиация

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