finrank_eq_rank — Mathlib

English

If M is finite as an R-module, then for every Submodule N of M, the finrank of N equals the rank of N.

Русский

Если M конечномерный R-модуль, то для каждого подмодуля N выполняется finrank R N = rank R N.

LaTeX

$$$\\operatorname{finrank} R N = \\operatorname{Module.rank} R N$$$

Lean4

/-- If `M` is finite, then `finrank N = rank N` for all `N : Submodule M`. Note that
such an `N` need not be finitely generated. -/
protected theorem _root_.Submodule.finrank_eq_rank [Module.Finite R M] (N : Submodule R M) :
    finrank R N = Module.rank R N :=
  by
  rw [finrank, Cardinal.cast_toNat_of_lt_aleph0]
  exact lt_of_le_of_lt (Submodule.rank_le N) (rank_lt_aleph0 R M)

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