English
A RingEquiv between R and S defines an R-linear equivalence between R and S as modules via the CompHom construction; this provides a natural bridge between ring and module structures.
Русский
Кольцевой эквивалент между R и S задает R-линейное эквивалентное отображение между соответствующими модулями через построение CompHom; обеспечивает естественный переход между кольцевыми и модульными структурами.
LaTeX
$$$ \text{Module.compHom}$$$
Lean4
/-- Each element of the group defines a module automorphism.
This is a stronger version of `DistribMulAction.toAddAut`. -/
@[simps]
def toModuleAut : S →* M ≃ₗ[R] M where
toFun := toLinearEquiv R M
map_one' := LinearEquiv.ext <| one_smul _
map_mul' _ _ := LinearEquiv.ext <| mul_smul _ _
