English
For a Group G acting on a monoid M with compatible SMul and IsScalarTower, the inverse of a smul acts as the smul by the group inverse on the inverse unit.
Русский
Для группы G, действующей на моноид M, с совместимым SMul и IsScalarTower, обратное от смула действует как смул группы на обратной единице.
LaTeX
$$$ (g \\cdot m)^{-1} = g^{-1} \\cdot m^{-1} $$$
Lean4
/-- Note that this lemma exists more generally as the global `smul_inv` -/
@[to_additive (attr := simp)]
theorem smul_inv [Group G] [Monoid M] [MulAction G M] [SMulCommClass G M M] [IsScalarTower G M M] (g : G) (m : Mˣ) :
(g • m)⁻¹ = g⁻¹ • m⁻¹ :=
ext rfl