spanFinrank_eq_iInf — Mathlib

English

The finite rank equals the iInf of the cardinalities of finite generating sets for p.

Русский

Конечная ранг равен iInf мощности конечных порождающих наборов p.

LaTeX

$$$\operatorname{spanFinrank}(p) = \operatorname{iInf}(\lambda s.\, |s|)$, where s ranges over finite generating sets with span R s = p.$$

Lean4

theorem spanFinrank_eq_iInf (p : Submodule R M) : p.spanFinrank = ⨅ (s : { s : Finset M // span R s = p }), s.1.card :=
  by simp [spanFinrank, Cardinal.toNat, spanRank_toENat_eq_iInf_finset_card, ENat.iInf_toNat]

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