map_multiset_ne_zero_prod

Mathlib.Algebra.BigOperators.Group.Multiset.Basic

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

← MathLib Explorer

English

If s ≠ 0, then f s.prod = (s.map f).prod for any functor f with the appropriate structure.

Русский

Если s ≠ 0, то для отображения f верно f(prod s) = prod(map f s).

LaTeX

$$$ (s.map f).prod = f\, s.prod $$$

Lean4

@[to_additive]
theorem _root_.map_multiset_ne_zero_prod [FunLike F M N] [MulHomClass F M N] (f : F) {s : Multiset M} (hs : s ≠ 0) :
    f s.prod = (s.map f).prod :=
  (s.prod_hom_ne_zero hs f).symm

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

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

Разделы

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

Аффилиация

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