finrank_quotient_add_finrank_le — Mathlib

English

For a submodule N of M, the sum of finrank of the quotient M/N and finrank of N does not exceed finrank of M.

Русский

Пусть N ⊆ M — подмодуль. Тогда finrank_R(M/N) + finrank_R(N) ≤ finrank_R(M).

LaTeX

$$$\\\\operatorname{finrank}_R(M/N) + \\\\operatorname{finrank}_R(N) \\\\le \\\\operatorname{finrank}_R(M).$$$

Lean4

/-- Similar to `rank_quotient_add_rank_le` but for `finrank` and a finite `M`. -/
theorem finrank_quotient_add_finrank_le (N : Submodule R M) : finrank R (M ⧸ N) + finrank R N ≤ finrank R M :=
  by
  haveI := nontrivial_of_invariantBasisNumber R
  have := rank_quotient_add_rank_le N
  rw [← finrank_eq_rank R M, ← finrank_eq_rank R, ← N.finrank_eq_rank] at this
  exact mod_cast this

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