leftInvEquiv_symm_eq_inv — Mathlib

English

In a commutative group, the symmetric of the leftInvEquiv evaluated on x equals the inverse of x: ((S.leftInvEquiv hS).symm x) = (x)^{-1}.

Русский

В коммутативной группе симметричный инвертированный эквивалентности leftInvEquiv дает обратное к x.

LaTeX

$$$ ((S.leftInvEquiv hS).symm x) = (x)^{-1} $$$

Lean4

@[to_additive (attr := simp)]
theorem leftInvEquiv_symm_eq_inv (x : S) : ((S.leftInvEquiv hS).symm x : M) = (x : M)⁻¹ := by
  rw [← mul_right_inj (x : M), mul_inv_cancel, mul_leftInvEquiv_symm]

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