English
If a group G acts on M and G acts on M compatibly, then there is a MulAction of G on Units M lifting the original action.
Русский
Если группа G действует на M и эти действия совместимы, существует MulAction G на Units M, поднимающий исходное действие.
LaTeX
$$$ \\text{MulAction } G\\, (Units M)$$$
Lean4
/-- If an action `G` associates and commutes with multiplication on `M`, then it lifts to an
action on `Mˣ`. Notably, this provides `MulAction Mˣ Nˣ` under suitable conditions. -/
@[to_additive]
instance mulAction' [Group G] [Monoid M] [MulAction G M] [SMulCommClass G M M] [IsScalarTower G M M] : MulAction G Mˣ
where
smul g
m :=
⟨g • (m : M), (g⁻¹ • ((m⁻¹ : Mˣ) : M)), by rw [smul_mul_smul_comm, Units.mul_inv, mul_inv_cancel, one_smul], by
rw [smul_mul_smul_comm, Units.inv_mul, inv_mul_cancel, one_smul]⟩
one_smul _ := Units.ext <| one_smul _ _
mul_smul _ _ _ := Units.ext <| mul_smul _ _ _
