English
If f: M → M₂ is injective, there exists a linear equivalence between M and its range given by f; in particular the forward map is f.
Русский
Если f: M → M₂ инъективно, существует линейное эквивалентное отображение между M и его образом f(M), заданное f; переходная карта равна f.
LaTeX
$$$\\text{If } f \\text{ is injective, then } M \\overset{f}{\\to} \\mathrm{range}(f) \\text{ is a linear equivalence.}$$$
Lean4
/-- An `Injective` linear map `f : M →ₗ[R] M₂` defines a linear equivalence
between `M` and `f.range`. See also `LinearMap.ofLeftInverse`. -/
noncomputable def ofInjective [RingHomInvPair σ₁₂ σ₂₁] [RingHomInvPair σ₂₁ σ₁₂] (h : Injective f) :
M ≃ₛₗ[σ₁₂] LinearMap.range f :=
ofLeftInverse <| Classical.choose_spec h.hasLeftInverse
