map_multiset_prod

Mathlib.Algebra.BigOperators.Group.Multiset.Basic

URI: https://scilib.ai/kg/mathlib#map_multiset_prod

← MathLib Explorer

English

For any map f, the product of the image equals the image of the product: f(s.prod) = (s.map f).prod.

Русский

Для отображения f верно: f(prod s) = prod(map f s).

LaTeX

$$$ f\, s.prod = \mathrm{prod}(s.map f) $$$

Lean4

@[to_additive]
theorem _root_.map_multiset_prod [FunLike F M N] [MonoidHomClass F M N] (f : F) (s : Multiset M) :
    f s.prod = (s.map f).prod :=
  (s.prod_hom f).symm

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

Научная платформа российской исследовательской школы.

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru