English
Each element of a group G acting on a monoid M induces a multiplicative monoid isomorphism of M, giving a map toMulEquiv: G → (Monoid automorphisms of M).
Русский
Каждому элементу группы G, действующей на моид M, соответствует мульти-монодный изоморфизм M, задающий отображение toMulEquiv: G → M ≃* M.
LaTeX
$$$\text{toMulEquiv} : G \to \mathrm{Aut}_{\mathrm{Mul}}(M) \;\; (G \text{ acting on } M).$$$
Lean4
/-- Each element of the group defines a multiplicative monoid isomorphism.
This is a stronger version of `MulAction.toPermHom`. -/
@[simps]
def toMulAut : G →* MulAut M where
toFun := MulDistribMulAction.toMulEquiv M
map_one' := MulEquiv.ext (one_smul _)
map_mul' _ _ := MulEquiv.ext (mul_smul _ _)
