congr — Mathlib

English

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

Русский

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

LaTeX

$$$\\forall a,b\\ (Invertible\\ a)\\ (Invertible\\ b),\\ a=b\\Rightarrow a^{-1}=b^{-1}$$$

Lean4

/-- If `a` is invertible and `a = b`, then `⅟a = ⅟b`. -/
@[congr]
theorem congr [Monoid α] (a b : α) [Invertible a] [Invertible b] (h : a = b) : ⅟a = ⅟b :=
  invertible_unique a b h

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