coe_multiset_prod — Mathlib

English

The Real embedding preserves product over a multiset: (s.prod)^\uparrow = (s.map (\uparrow)).prod.

Русский

Преобразование Real сохраняет произведение мультимножества: (s.prod)^\uparrow = (s.map (\uparrow)).prod.

LaTeX

$$$ (s.prod \\\\text{ : }\\\\mathbb{R}_{\\\\ge 0})^{\\\\uparrow} = (s.map (\\\\uparrow)).\\\\text{prod}. $$$

Lean4

@[norm_cast]
theorem coe_multiset_prod (s : Multiset ℝ≥0) : ((s.prod : ℝ≥0) : ℝ) = (s.map (↑)).prod :=
  map_multiset_prod toRealHom s

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