spanRank — Mathlib

English

If v: ι → M is an injective family that is linearly independent, then the span of its range has rank equal to the cardinality of ι: span R(range v) has rank |ι|.

Русский

Если v: ι → M — инъективная линейно независимая семейство, тогда порождаемое им множество имеет ранг, равный мощности множества индексов: span R(range v) имеет ранг |ι|.

LaTeX

$$$\text{spanRank}(\operatorname{span} R(\{\text{range}(v)\})) = |\iota|.$$$

Lean4

/-- The minimum cardinality of a generating set of a submodule as a cardinal. -/
noncomputable def spanRank (p : Submodule R M) : Cardinal :=
  ⨅ (s : { s : Set M // span R s = p }), #s

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