mulLeft_symm_apply — Mathlib

English

The inverse of the left-translation by a is left-translation by a^{-1}.

Русский

Обратное к левому умножению на a — левое умножение на a^{-1}.

LaTeX

$$$(L_a)^{-1} = L_{a^{-1}}$$$

Lean4

/-- Extra simp lemma that `dsimp` can use. `simp` will never use this. -/
@[to_additive (attr := simp) /-- Extra simp lemma that `dsimp` can use. `simp` will never use this. -/
    ]
theorem mulLeft_symm_apply (a : G) : ((Equiv.mulLeft a).symm : G → G) = (a⁻¹ * ·) :=
  rfl

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