x is invertible if it has left inverse

Stream: Is there code for X?

[Kenny Lau]

import Mathlib

def Invertible.ofMulRight {α : Type u} [CommMonoid α] {a : α} (b : α) (h : a * b = 1) : Invertible a :=
  ⟨b, h ▸ mul_comm b a, h⟩

def Invertible.ofMulLeft {α : Type u} [CommMonoid α] {a : α} (b : α) (h : b * a = 1) : Invertible a :=
  ⟨b, h, h ▸ mul_comm a b⟩

[Eric Wieser]

These are defs so the name should avoid _

[Kenny Lau]

edited