prod_mk — Mathlib

English

The product of a multiset mapped by Associates.mk equals the Associates.mk of the product of the multiset.

Русский

Произведение мультисета после отображения через mk равно mk от произведения элементов мультисета.

LaTeX

$$({p : Multiset M}) → (p.map Associates.mk).prod = Associates.mk p.prod$$

Lean4

theorem prod_mk {p : Multiset M} : (p.map Associates.mk).prod = Associates.mk p.prod :=
  Multiset.induction_on p (by simp) fun a s ih => by simp [ih, Associates.mk_mul_mk]

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