spanRank_span_of_linearIndepOn — Mathlib

English

If v: ι → M is injective and linearly independent, then the span of its range has rank equal to cardinality of ι.

Русский

Если v: ι → M инъективен и линейно независим, то порождаемая им линейная оболочка имеет ранг равный мощности ι.

LaTeX

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

Lean4

theorem spanRank_span_of_linearIndepOn [RankCondition R] (s : Set M) (hs : LinearIndepOn R id s) :
    (span R s).spanRank = #s := by simp [← spanRank_span_range_of_linearIndependent Subtype.val_injective hs]

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