iSupIndep_iff_linearIndependent_of_ne_zero

English

Equivalence between iSupIndep of spans and linear independence of the generating vectors.

Русский

Эквивалентность между iSupIndep порождаемых подмодулей и линейной независимостью порождающих векторов.

LaTeX

$$iSupIndep (fun i => Submodule.span R (Set.singleton (v i)))$$

Lean4

theorem iSupIndep_iff_linearIndependent_of_ne_zero [NoZeroSMulDivisors R N] {ι} {v : ι → N} (h_ne_zero : ∀ i, v i ≠ 0) :
    (iSupIndep fun i => R ∙ v i) ↔ LinearIndependent R v :=
  let _ := Classical.decEq ι
  ⟨fun hv => hv.linearIndependent _ (fun i => Submodule.mem_span_singleton_self <| v i) h_ne_zero, fun hv =>
    hv.iSupIndep_span_singleton⟩

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