finiteDimensional_range — Mathlib

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

/-- The range of a linear map defined on a finite-dimensional space is also finite-dimensional. -/
instance finiteDimensional_range [FiniteDimensional K V] (f : V →ₗ[K] V₂) : FiniteDimensional K (LinearMap.range f) :=
  Module.Finite.range f

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