Submodule Basis

This file provides auxilliary lemmas for proving Matrix.exists_standardRepr_isBase via the subspace generated by a matrix.

theorem Basis.linearIndepOn_in_submodule {α : Type u_1} {R : Type u_2} [Ring R] {X Y G I : Set α} {A : Matrix (↑X) (↑Y) R} {hIX : I ⊆ X} (B : Basis (↑G) R ↥(Submodule.span R A.range)) (hAI : LinearIndepOn R A hIX.elem.range) : LinearIndepOn R (fun (x : ↑X) (g : ↑G) => (B.repr ⟨A x, ⋯⟩) g) hIX.elem.range

theorem Basis.linearIndepOn_of_in_submodule {α : Type u_1} {R : Type u_2} [Ring R] {X Y G I : Set α} {A : Matrix (↑X) (↑Y) R} {hIX : I ⊆ X} (B : Basis (↑G) R ↥(Submodule.span R A.range)) (hBI : LinearIndepOn R (fun (x : ↑X) (g : ↑G) => (B.repr ⟨A x, ⋯⟩) g) hIX.elem.range) : LinearIndepOn R A hIX.elem.range