invOf_eq_left_inv — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

theorem invOf_eq_left_inv [Monoid α] {a b : α} [Invertible a] (hac : b * a = 1) : ⅟a = b :=
  (left_inv_eq_right_inv hac (mul_invOf_self _)).symm

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