linearEquivOfLeftInverse — Mathlib

English

If f is left inverse of g, then f is also right inverse of g, yielding a linear equivalence.

Русский

Если f является левым обратным к g, то f также является правым обратным к g, в результате получается линейное эквивалентное отображение.

LaTeX

$$LeftInverse f g → RightInverse f g$$

Lean4

/-- If `f : M →ₗ[R] N` and `g : N →ₗ[R] M` where `M` and `N` are invertible `R`-modules, and `f` is
a left inverse of `g`, then in fact `f` is also the right inverse of `g`, and we promote this to
an `R`-module isomorphism. -/
def linearEquivOfLeftInverse (hfg : Function.LeftInverse f g) : M ≃ₗ[R] N :=
  .ofLinear f g (LinearMap.ext hfg) (LinearMap.ext <| rightInverse_of_leftInverse hfg)

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