multinomial_congr — Mathlib

English

If f and g agree on s, then multinomial s f = multinomial s g.

Русский

Если функции f и g совпадают на s, тогда multinomial s f = multinomial s g.

LaTeX

$$$ \\text{multinomial}(s,f) = \\text{multinomial}(s,g) \\quad\\text{if } \\forall a \\in s,\\ f(a)=g(a). $$$

Lean4

theorem multinomial_congr {f g : α → ℕ} (h : ∀ a ∈ s, f a = g a) : multinomial s f = multinomial s g :=
  by
  simp only [multinomial]; congr 1
  · rw [Finset.sum_congr rfl h]
  · exact Finset.prod_congr rfl fun a ha => by rw [h a ha]

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