English
For any submodule p of M, there exists a subset S of M such that span_R(S) = p and the cardinality of S equals spanRank(p); the chosen set is a generating set of minimal cardinality for p.
Русский
Для любого подпространства p ⊆ M существует множество S ⊆ M такое, что span_R(S) = p и кардинал(S) = spanRank(p); выбранный набор порождает p минимальной по кардинальности.
LaTeX
$$$\exists S \subseteq M,\; \operatorname{span}_R(S) = p \land \#S = \operatorname{spanRank}(p).$$$
Lean4
/-- Generating elements for the submodule of minimum cardinality. -/
noncomputable def generators (p : Submodule R M) : Set M :=
Classical.choose (exists_span_set_card_eq_spanRank p)
