English
For a group G acting on α, the comapSMul action on Finsupp α M is implemented by precomposition with the inverse action. Consequently, (g • f)(a) = f(g^{-1} • a).
Русский
Для группы G, действующей на α, операция comapSMul на Finsupp α M реализуется через предсоставление с обратным действием: (g • f)(a) = f(g^{-1} • a).
LaTeX
$$$ (g \\cdot f)(a) = f(g^{-1} \\cdot a) $$$
Lean4
/-- When `G` is a group, `Finsupp.comapSMul` acts by precomposition with the action of `g⁻¹`.
-/
@[simp]
theorem comapSMul_apply (g : G) (f : α →₀ M) (a : α) : (g • f) a = f (g⁻¹ • a) :=
by
conv_lhs => rw [← smul_inv_smul g a]
exact mapDomain_apply (MulAction.injective g) _ (g⁻¹ • a)
