English
The map g ↦ mulIndicator s g is a monoid hom from the monoid of all functions α → M (with pointwise multiplication) to the same monoid of functions α → M.
Русский
Отображение g ↦ mulIndicator s g является гомоморфизмом моноида: оно сохраняет единицу и произведение на множестве функций α → M.
LaTeX
$$$$ \\text{mulIndicatorHom } M s: (\\alpha \\to M) \\to_* (\\alpha \\to M) \\quad\\text{is a MonoidHom} \\bigl( g \\mapsto mulIndicator s g \\bigr). $$$$
Lean4
/-- `Set.mulIndicator` as a `monoidHom`. -/
@[to_additive /-- `Set.indicator` as an `addMonoidHom`. -/
]
noncomputable def mulIndicatorHom {α} (M) [MulOneClass M] (s : Set α) : (α → M) →* α → M
where
toFun := mulIndicator s
map_one' := mulIndicator_one M s
map_mul' := mulIndicator_mul s
