invertible_unique — Mathlib

English

If a = b with a and b invertible, then their inverses coincide: a^{-1} = b^{-1}.

Русский

Если a = b и оба обратимы, то их обраты совпадают: a^{-1} = b^{-1}.

LaTeX

$$$\\forall \\alpha\\ (Monoid\\ \\alpha),\\forall a,b\\in\\alpha\\,[Invertible\\ a][Invertible\\ b],\\ a=b\\Rightarrow a^{-1}=b^{-1}$$$

Lean4

theorem invertible_unique {α : Type u} [Monoid α] (a b : α) [Invertible a] [Invertible b] (h : a = b) : ⅟a = ⅟b :=
  by
  apply invOf_eq_right_inv
  rw [h, mul_invOf_self]

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