cast_multiset_prod — Mathlib

English

Let α be a Field and s a multiset of rationals. Then the cast of the product over s equals the product of the casts: (↑(s.prod)) = (s.map ↑).prod.

Русский

Пусть α — поле, и s — мультисет рациональных чисел. Тогда приведение произведения по s равно произведению приведённых элементов.

LaTeX

$$$ \left( \mathrm{prod}\, s \right)^{\uparrow} = \mathrm{prod}(\mathrm{map}(\uparrow)\, s). $$$

Lean4

@[simp, norm_cast]
theorem cast_multiset_prod (s : Multiset ℚ) : (↑s.prod : α) = (s.map (↑)).prod :=
  map_multiset_prod (Rat.castHom α) _

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