invOf_eq_right_inv — Mathlib

English

Let α be a Monoid and a ∈ α be invertible. If there exists b ∈ α with a b = 1, then a^{-1} = b.

Русский

Пусть α — моноид, элемент a ∈ α обратим. Если существует b ∈ α such that a b = 1, тогда a^{-1} = b.

LaTeX

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

Lean4

theorem invOf_eq_right_inv [Monoid α] {a b : α} [Invertible a] (hac : a * b = 1) : ⅟a = b :=
  left_inv_eq_right_inv (invOf_mul_self _) hac

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