# Commit 2024-04-13 12:00 7a71e528

View on Github →Feat (GroupTheory/GroupAction/Hom/Pointwise) : generalize smul set lemmas to group actions (#12023)
This is a generalization of `Mathlib/Algebra/Module/LinearMap/Pointwise.lean`

from `LinearMapClass`

to `MulActionHomClass`

.
The preexisting lemmas are generalized.

`image_smul_setₛₗ`

: under a`σ`

-equivariant map, one has`h '' (c • s) = (σ c) • h '' s`

.`preimage_smul_setₛₗ'`

is a general version of the equality`h ⁻¹' (σ c • s) = c • h⁻¹' s`

. It requires that`c`

acts surjectively and`σ c`

acts injectively. It is provided with specific versions:`preimage_smul_setₛₗ_of_units`

requires that`c`

and`σ c`

are units`MonoidHom.preimage_smul_setₛₗ`

requires that`σ`

is a`MonoidHom`

and`c`

is a unit`MonoidHomClass.preimage_smul_setₛₗ`

requires that`σ`

belongs to a`MonoidHomClass`

and that`c`

is a unit`Group.preimage_smul_setₛₗ`

requires that the types of`c`

and`σ c`

are groups`image_smul_set`

,`preimage_smul_set`

and`Group.preimage_smul_set`

are the variants when`σ`

is the identity.