length_le_of_injective — Mathlib

English

If f: N → M is an injective linear map, then the length of N does not exceed the length of M: length_R(N) ≤ length_R(M).

Русский

Если линейное отображение f: N → M инъективно, то длина N не превосходит длину M: length_R(N) ≤ length_R(M).

LaTeX

$$$\operatorname{length}_R(N) \le \operatorname{length}_R(M)$$$

Lean4

theorem length_le_of_injective : Module.length R N ≤ Module.length R M :=
  by
  rw [Module.length_eq_add_of_exact f (LinearMap.range f).mkQ hf (Submodule.mkQ_surjective _)
      (LinearMap.exact_map_mkQ_range f)]
  exact le_self_add

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