multinomial_eq — Mathlib

English

For any f: α →₀ ℕ, the finsupp-based multinomial coincides with the standard multinomial applied to the finite support and its values.

Русский

Для любого f: α →₀ ℕ мультиномиал на основе finsupp совпадает с обычным мультиномиалом, применяемым к опоре и её значениям.

LaTeX

$$$f.multinomial = \mathrm{Nat}.multinomial\; f\mathop{\mathrm{support}} f$$$

Lean4

theorem multinomial_eq (f : α →₀ ℕ) : f.multinomial = Nat.multinomial f.support f :=
  rfl

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