mulLeft_symm — Mathlib

English

For any x ∈ G, the isometry mulLeft x has inverse mulLeft x^{-1}; i.e., (mulLeft x)^{-1} = mulLeft x^{-1}.

Русский

Для любого x ∈ G изометрия mulLeft x имеет обратную mulLeft x^{-1}; то есть (mulLeft x)^{-1} = mulLeft x^{-1}.

LaTeX

$$$(\mathrm{mulLeft}\,x)^{-1} = \mathrm{mulLeft}\,x^{-1}$$$

Lean4

@[to_additive (attr := simp)]
theorem mulLeft_symm [IsIsometricSMul G G] (x : G) : (mulLeft x).symm = IsometryEquiv.mulLeft x⁻¹ :=
  constSMul_symm x

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