English
On a finite-dimensional space, a linear map is injective iff it is surjective.
Русский
На конечномерном пространстве линейное отображение инъективно тогда и только тогда, когда оно сюръективно.
LaTeX
$$$[\operatorname{FiniteDimensional}_K V] \\ {f : V \to V} : \operatorname{Injective} f \iff \operatorname{Surjective} f$$$
Lean4
/-- On a finite-dimensional space, a linear map is injective if and only if it is surjective. -/
theorem injective_iff_surjective [FiniteDimensional K V] {f : V →ₗ[K] V} : Injective f ↔ Surjective f :=
⟨surjective_of_injective, fun hsurj =>
let ⟨g, hg⟩ := f.exists_rightInverse_of_surjective (range_eq_top.2 hsurj)
have : Function.RightInverse g f := LinearMap.ext_iff.1 hg
(leftInverse_of_surjective_of_rightInverse (surjective_of_injective this.injective) this).injective⟩
