English
Let R be a Monoid and M an AddCommMonoid with a DistribMulAction of R. Then the unit group R^× acts on the nonzero elements of M by multiplying inside M; i.e. there is a canonical action of R^× on { x ∈ M | x ≠ 0 } given by a · x = a · x, satisfying (ab) · x = a · (b · x) and 1 · x = x.
Русский
Пусть R — моноид, M — добавочно коммутированное моноидное множество, на которое действует R по распределённому действию. Тогда группа единиц R^× действует на множества ненулевых элементов M: { x ∈ M | x ≠ 0 }, причём действие задаётся (а, x) ↦ a · x и удовлетворяет (ab) · x = a · (b · x), 1 · x = x.
LaTeX
$$$ (R^{\\times}) \\curvearrowright \\{ x \\in M \\mid x \\neq 0 \\} \\quad\\text{with}\\quad (a,x) \\mapsto a \\cdot x,\\quad (ab) \\cdot x = a \\cdot (b \\cdot x),\\quad 1 \\cdot x = x. $$$
Lean4
instance : MulAction Rˣ { x : M // x ≠ 0 } :=
SubMulAction.mulAction' (nonZeroSubMul R M)
