English
Let M and α be monoids and suppose α carries a distributive M-action. Then the group of units Mˣ acts on α by the natural inclusion (u acts as (u : M) • a), giving a MulDistribMulAction Mˣ α. In particular, for any u ∈ Mˣ and a,b ∈ α, u • (a b) = (u • a)(u • b) and u • 1 = 1.
Русский
Пусть M и α — моноиды, и пусть α имеет распределённое по M действие. Тогда группа единиц Mˣ действует на α естественным образом через включение (u действует как (u : M) • a), образуя MulDistribMulAction Mˣ α. То есть для любых u ∈ Mˣ и a,b ∈ α выполняются u • (a b) = (u • a)(u • b) и u • 1 = 1.
LaTeX
$$$\\exists \\text{MulDistribMulAction}(M^\\times, \\alpha) \\text{ with } (u,a) \\mapsto (u:M) \\cdot a, \\; u \\cdot (ab)=(u\\cdot a)(u\\cdot b), \\ u\\cdot 1=1.$$$
Lean4
instance instMulDistribMulAction [Monoid M] [Monoid α] [MulDistribMulAction M α] : MulDistribMulAction Mˣ α
where
smul_mul m := smul_mul' (m : M)
smul_one m := smul_one (m : M)
