invOf_eq_inv — Mathlib

English

For an invertible element x, the quasi-inverse ⅟x equals the standard inverse x^{-1}.

Русский

Для обратимого элемента x обратное в смысле ⅟x совпадает с обычным обратным x^{-1}.

LaTeX

$$$ [Invertible x] \\Rightarrow \\ \\⅟x = x^{-1} $$$

Lean4

@[simp]
theorem invOf_eq_inv (x : tsze R M) [Invertible x] : ⅟x = x⁻¹ :=
  by
  letI := invertibleFstOfInvertible x
  ext <;> simp [fst_invOf, snd_invOf]

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