English
If f and g are maps with a left inverse relation, then Invertible(f r) is equivalent to Invertible(r).
Русский
Если существуют отображения f и g с левой обратной связью, то Invertible(f(r)) эквивалентно Invertible(r).
LaTeX
$$$\text{Invertible}(f(r)) \iff \text{Invertible}(r)$$$
Lean4
/-- Invertibility on either side of a monoid hom with a left-inverse is equivalent. -/
@[simps]
def invertibleEquivOfLeftInverse {R : Type*} {S : Type*} {F G : Type*} [Monoid R] [Monoid S] [FunLike F R S]
[MonoidHomClass F R S] [FunLike G S R] [MonoidHomClass G S R] (f : F) (g : G) (r : R)
(h : Function.LeftInverse g f) : Invertible (f r) ≃ Invertible r
where
toFun _ := Invertible.ofLeftInverse f _ _ h
invFun _ := Invertible.map f _
left_inv _ := Subsingleton.elim _ _
right_inv _ := Subsingleton.elim _ _
