rank_span — Mathlib

English

If v is a linearly independent family, then the rank of the span of range(v) equals the cardinality of range(v): rank_R(span_R(range v)) = |range v|.

Русский

Для линейно независимого вектора, ранг порождаемого им модуля равен кардиналу диапазона: rank_R(span_R(range v)) = |range v|.

LaTeX

$$\\operatorname{rank}_R(\\operatorname{span}_R(\\mathrm{range}(v))) = |\\mathrm{range}(v)|$$

Lean4

theorem rank_span {v : ι → M} (hv : LinearIndependent R v) : Module.rank R ↑(span R (range v)) = #(range v) :=
  by
  haveI := nontrivial_of_invariantBasisNumber R
  rw [← Cardinal.lift_inj, ← (Basis.span hv).mk_eq_rank,
    Cardinal.mk_range_eq_of_injective (@LinearIndependent.injective ι R M v _ _ _ _ hv)]

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