English
If p is finitely generated, then the generating set p.generators has cardinality equal to spanFinrank(p).
Русский
Если p конечно порождается, то множество порождающих p.generators имеет кардинал, равный spanFinrank(p).
LaTeX
$$$(\mathrm{generators}(p)).\mathrm{ncard} = \operatorname{spanFinrank}(p).$$$
Lean4
theorem generators_ncard {p : Submodule R M} (h : p.FG) : (generators p).ncard = spanFinrank p :=
by
rw [← Nat.cast_inj (R := Cardinal), ← fg_iff_spanRank_eq_spanFinrank.mpr h, Set.ncard, Set.encard, ENat.card,
generators_card, toNat_toENat, ← spanFinrank]
exact (fg_iff_spanRank_eq_spanFinrank.mpr h).symm