ofInjectiveEndo — Mathlib

English

An injective linear map between finite-dimensional modules of equal rank is a linear equivalence.

Русский

Инъективное линейное отображение между конечномерными модулями с равной размерностью является линейным эквивалентом.

LaTeX

$$$f: V \to V'$, injective, and $\operatorname{finrank}_K V = \operatorname{finrank}_K V'\Rightarrow f \text{ is a linear equivalence } V \cong_K V'$$$

Lean4

/-- The linear equivalence corresponding to an injective endomorphism. -/
noncomputable def ofInjectiveEndo (f : V →ₗ[K] V) (h_inj : Injective f) : V ≃ₗ[K] V :=
  LinearEquiv.ofBijective f ⟨h_inj, LinearMap.injective_iff_surjective.mp h_inj⟩

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