smul_inv — Mathlib

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

Похожие утверждения