prod_mk — Mathlib

English

If s is a Multiset with Nodup, then the Finset built as ⟨s,Nodup⟩ has the same product as the Multiset s mapped by f: (⟨s,Nodup⟩).prod f = (s.map f).prod.

Русский

Если s имеет свойство Nodup, то произведение финсета, построенного как ⟨s,Nodup⟩, равно произведению мультимножества s, отображенного через f: (⟨s,Nodup⟩).prod f = (s.map f).prod.

LaTeX

$$$$ (\\langle s, \\mathrm{nodup} \\rangle : \\mathrm{Finset}\\; \\iota).prod f = (s.map f).prod. $$$$

Lean4

@[to_additive (attr := simp)]
theorem prod_mk [CommMonoid M] (s : Multiset ι) (hs : s.Nodup) (f : ι → M) :
    (⟨s, hs⟩ : Finset ι).prod f = (s.map f).prod :=
  rfl

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