Left_and_Right_Inverses_of_Product
Provedmonoidsproofwiki
In a monoid, if xy has a left inverse and yx has a right inverse, then both x and y are invertible.
Preamble
import Mathlib.Algebra.Group.Defs
Formal statement
theorem Left_and_Right_Inverses_of_Product {M : Type _} [Monoid M] (x y : M) (hL : ∃ zL : M, zL * (x * y) = 1) (hR : ∃ zR : M, (y * x) * zR = 1) : (∃ xi : M, xi * x = 1 ∧ x * xi = 1) ∧ (∃ yi : M, yi * y = 1 ∧ y * yi = 1) := by sorrySource