prod_hom_ne_zero

Mathlib.Algebra.BigOperators.Group.Multiset.Basic

URI: https://scilib.ai/kg/mathlib#Multiset.prod_hom_ne_zero

← MathLib Explorer

English

If s ≠ 0 and f is a monoid hom, then (map f s).prod = f s.prod.

Русский

Если s ≠ 0 и f — гомоморфизм моноида, то prod(m.map f) = f(prod s).

LaTeX

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

Lean4

@[to_additive]
theorem prod_hom_ne_zero {s : Multiset M} (hs : s ≠ 0) {F : Type*} [FunLike F M N] [MulHomClass F M N] (f : F) :
    (s.map f).prod = f s.prod := by induction s using Quot.inductionOn; aesop (add simp List.prod_hom_nonempty)

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

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

Разделы

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

Аффилиация

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