English
If G is a group, M a monoid, and M carries a distributive G-action with SMulCommClass and IsScalarTower conditions, then the units Mˣ inherit a distributive action of G, defined by smul := (· • ·). This means for g in G and u,v in Mˣ, g • (uv) = (g • u)(g • v) and g • 1 = 1.
Русский
Если G — группа, M — моноид, и M поддерживает распределимое действие G с условиями SMulCommClass и IsScalarTower, то единицы Mˣ наследуют распределимое действие G, определённое как smul := (· • ·). То же для всех g ∈ G и u,v ∈ Mˣ выполняются g • (uv) = (g • u)(g • v) и g • 1 = 1.
LaTeX
$$$\\exists \\text{MulDistribMulAction } G\\; M^{\\times} \\text{ with } g\\colon G, u\\in M^{\\times}: (g\\cdot u) = \\text{Units.map } (\\lambda x. g \\cdot x) u, \\ (g\\cdot (uv))=(g\\cdot u)(g\\cdot v),\\ g\\cdot 1 = 1.$$$
Lean4
/-- A stronger form of `Units.mul_action'`. -/
instance mulDistribMulAction' [Group G] [Monoid M] [MulDistribMulAction G M] [SMulCommClass G M M]
[IsScalarTower G M M] : MulDistribMulAction G Mˣ :=
{ Units.mulAction' with smul := (· • ·), smul_one := fun _ => Units.ext <| smul_one _,
smul_mul := fun _ _ _ => Units.ext <| smul_mul' _ _ _ }
