English
If the span of the ranges of a family v spans the whole space and f ∘ v is linearly independent, then f is injective.
Русский
Если линейная оболочка образов v охватывает всю пространство, а набор f ∘ v линейно независим, то f инъективно.
LaTeX
$$$ \\operatorname{span} R (\\operatorname{range} v) = \\top \\quad\\wedge\\quad \\text{LinearIndependent}_R (f \\circ v) \\Rightarrow \\text{Injective} (f) $$$
Lean4
/-- Given a linear map `f` between two vector spaces with the same dimension, if
`ker f = ⊥` then `linearEquivOfInjective` is the induced isomorphism
between the two vector spaces. -/
noncomputable def linearEquivOfInjective [FiniteDimensional K V] [FiniteDimensional K V₂] (f : V →ₗ[K] V₂)
(hf : Injective f) (hdim : finrank K V = finrank K V₂) : V ≃ₗ[K] V₂ :=
LinearEquiv.ofBijective f ⟨hf, (LinearMap.injective_iff_surjective_of_finrank_eq_finrank hdim).mp hf⟩
