rank_range_of_injective — Mathlib

English

If f is injective, then the rank of the range of f equals the rank of M (unlifted).

Русский

Если f инъективно отображает M в M', то ранг образа совпадает с рангом M (без подъема вселенной).

LaTeX

$$$\operatorname{Module.rank} R (\operatorname{range} f) = \operatorname{Module.rank} R M$$$

Lean4

theorem rank_range_of_injective (f : M →ₗ[R] M₁) (h : Injective f) :
    Module.rank R (LinearMap.range f) = Module.rank R M :=
  (LinearEquiv.ofInjective f h).rank_eq.symm

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