English
The finite rank of a submodule equals the infimum of the cardinalities of finite generating sets: spanFinrank(p) = inf{ card(s) : s is a Finset with span R s = p }.
Русский
Конечная ранговая характеристика подпространения равнаInf мощности конечных порождающих наборов: spanFinrank(p) = inf{ card(s) : s — конечный набор, span R s = p }.
LaTeX
$$$\operatorname{spanFinrank}(p) = \inf\{ |s| : s \text{ is a finite set with } \operatorname{span} R s = p \}.$$$
Lean4
/-- The minimum cardinality of a generating set of a submodule as a natural number. If no finite
generating set exists, the span rank is defined to be `0`. -/
noncomputable def spanFinrank (p : Submodule R M) : ℕ :=
(spanRank p).toNat
