rank_range_of_surjective — Mathlib

English

If f is surjective, then the rank of the range equals the rank of the codomain.

Русский

Если f сюръективно отображает M на M', то ранг образа равен рангу пространства дописьания.

LaTeX

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

Lean4

theorem rank_range_of_surjective (f : M →ₗ[R] M') (h : Surjective f) :
    Module.rank R (LinearMap.range f) = Module.rank R M' := by rw [LinearMap.range_eq_top.2 h, rank_top]

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