finrank_range_of_inj — Mathlib

English

For an injective linear map f : M →ₗ[R] N, finrank of the range equals finrank of M.

Русский

Для инъективного линейного отображения f: M →ₗ[R] N выполняется finrank R (Range f) = finrank R M.

LaTeX

$$$\\operatorname{finrank}_R (\\operatorname{LinearMap.range} f) = \\operatorname{finrank}_R M$$$

Lean4

/-- The dimensions of the domain and range of an injective linear map are equal. -/
theorem finrank_range_of_inj {f : M →ₗ[R] N} (hf : Function.Injective f) :
    finrank R (LinearMap.range f) = finrank R M := by rw [(LinearEquiv.ofInjective f hf).finrank_eq]

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