finrank_le_finrank_of_injective — Mathlib

English

If f: M → M' is an injective linear map of finite R-modules, then finrank R M ≤ finrank R M'.

Русский

Пусть f: M → M' — инъективное линейное отображение между конечномерными R-модулями. Тогда finrank R M ≤ finrank R M'.

LaTeX

$$$\\operatorname{finrank} R M \\le \\operatorname{finrank} R M'$$$

Lean4

theorem finrank_le_finrank_of_injective [Module.Finite R M'] {f : M →ₗ[R] M'} (hf : Function.Injective f) :
    finrank R M ≤ finrank R M' :=
  finrank_le_finrank_of_rank_le_rank (LinearMap.lift_rank_le_of_injective _ hf) (rank_lt_aleph0 _ _)

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