cast_multisetProd — Mathlib

English

For any multiset s of nonnegative rationals, the cast of the product equals the product of the casts.

Русский

Для любого мульти-множества s ℚ≥0 привод произведения равен произведению приводов элементов.

LaTeX

$$$(s.prod)^{\uparrow} = (s.map (\uparrow)).prod$$$

Lean4

@[norm_cast]
theorem cast_multisetProd (s : Multiset ℚ≥0) : (s.prod : K) = (s.map (↑)).prod :=
  map_multiset_prod (castHom _) _

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