prod_toEnumFinset — Mathlib

English

For a multiset m of α and a function f: α → ℕ → β, the product over toEnumFinset of f(x.1)(x.2) equals the product over x : m of f x x.2.

Русский

Пусть m — мультимножество над α и f: α → ℕ → β. Тогда произведение по toEnumFinset от f(x.1)(x.2) равно произведению по x ∈ m от f x x.2.

LaTeX

$$$ \prod x \in m.\mathrm{toEnumFinset}, f x.1 x.2 = \prod x : m, f x x.2 $$$

Lean4

@[to_additive]
theorem prod_toEnumFinset {β : Type*} [CommMonoid β] (m : Multiset α) (f : α → ℕ → β) :
    ∏ x ∈ m.toEnumFinset, f x.1 x.2 = ∏ x : m, f x x.2 :=
  by
  rw [Fintype.prod_equiv m.coeEquiv (fun x ↦ f x x.2) fun x ↦ f x.1.1 x.1.2]
  · rw [← m.toEnumFinset.prod_coe_sort fun x ↦ f x.1 x.2]
  · intro x
    rfl

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