rank_range_le — Mathlib

English

The rank of the range of a linear map is bounded by the rank of the domain after lifting.

Русский

Ранг образа линейного отображения ограничен рангом домена после подъема.

LaTeX

$$$\operatorname{rank}_R(\operatorname{range} f) \le \operatorname{rank}_R(M)$$$

Lean4

theorem rank_range_le (f : M →ₗ[R] M₁) : Module.rank R (LinearMap.range f) ≤ Module.rank R M := by
  simpa using lift_rank_range_le f

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