length_le_of_surjective — Mathlib

English

If g: M → P is surjective, then the length of P does not exceed the length of M: length_R(P) ≤ length_R(M).

Русский

Если g: M → P сюръективно, то длина P не превосходит длины M: length_R(P) ≤ length_R(M).

LaTeX

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

Lean4

theorem length_le_of_surjective : Module.length R P ≤ Module.length R M :=
  by
  rw [Module.length_eq_add_of_exact (LinearMap.ker g).subtype g (Submodule.subtype_injective _) hg
      (LinearMap.exact_subtype_ker_map g)]
  exact le_add_self

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