rank_map_le — Mathlib

English

Let f: M →_R M' be a linear map and p a submodule of M. Then the rank of the image p.map f is at most the rank of p.

Русский

Пусть f: M →_R M' — линейное отображение, p — подмодуль M. Тогда ранг образа p под действием f не превосходит ранг p.

LaTeX

$$$\operatorname{Module.rank} R (p.map f) \le \operatorname{Module.rank} R p$$$

Lean4

theorem rank_map_le (f : M →ₗ[R] M₁) (p : Submodule R M) : Module.rank R (p.map f) ≤ Module.rank R p := by
  simpa using lift_rank_map_le f p

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