snd_prod — Mathlib

English

Let s be a finite multiset of ordered pairs (x, y). Then the second component of the product over s equals the product of the second components.

Русский

Пусть s — конечная мультисетка пар (x, y). Тогда вторая координата произведения по s равна произведению вторых координат.

LaTeX

$$$\\left( \\prod s \\right)_2 = \\left( \\prod (s.map \\mathrm{snd}) \\right)$$$

Lean4

@[to_additive]
theorem snd_prod (s : Multiset (M × N)) : s.prod.2 = (s.map Prod.snd).prod :=
  map_multiset_prod (MonoidHom.snd _ _) _

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