English
Let G be a monoid acting on α and M be an additive commutative monoid. There is a natural action of G on the finsupp space α →₀ M, obtained by precomposing the action on α (via comapSMul). In particular, this makes α →₀ M into a MulAction of G.
Русский
Пусть G — моноид, действующий на множество α, и M — добавочно-коммутативный моноид. Существует естественное действие G на пространство Finsupp α M, полученное путём предварительной композиции с действием на α. Это даёт структуру MulAction на α →₀ M.
LaTeX
$$$\text{MulAction } G\, (\alpha \to_0 M)$$$
Lean4
/-- `Finsupp.comapSMul` is multiplicative -/
def comapMulAction : MulAction G (α →₀ M)
where
one_smul f := by rw [comapSMul_def, one_smul_eq_id, mapDomain_id]
mul_smul g g' f := by rw [comapSMul_def, comapSMul_def, comapSMul_def, ← comp_smul_left, mapDomain_comp]
