finrank_map_le — Mathlib

English

Pushforwards of finite submodules have a smaller finrank: finrank(p.map f) ≤ finrank(p).

Русский

Образ подпространства при линейном отображении f из p имеет размерность не большую, чем размерность p: finrank(p.map f) ≤ finrank(p).

LaTeX

$$$ \\text{finrank}_R(p.map f) \\leq \\text{finrank}_R(p). $$$

Lean4

/-- Pushforwards of finite submodules have a smaller finrank. -/
theorem finrank_map_le [Module R M'] (f : M →ₗ[R] M') (p : Submodule R M) [Module.Finite R p] :
    finrank R (p.map f) ≤ finrank R p :=
  finrank_le_finrank_of_rank_le_rank (lift_rank_map_le _ _) (rank_lt_aleph0 _ _)

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