finrank_quotient_le — Mathlib

English

The collection of ranks over all scalars yields a bound on the total rank.

Русский

Собрание рангов по всем скалярам задаёт верхнюю границу для общего ранга.

LaTeX

$$$\text{ciSup}_{s} \operatorname{rank} = \dots$$$

Lean4

/-- The dimension of a quotient is bounded by the dimension of the ambient space. -/
theorem finrank_quotient_le [StrongRankCondition R] [Module.Finite R M] (s : Submodule R M) :
    finrank R (M ⧸ s) ≤ finrank R M :=
  toNat_le_toNat ((Submodule.mkQ s).rank_le_of_surjective Quot.mk_surjective) (rank_lt_aleph0 _ _)

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