Submodule Spans

This file provides lemmas about the linear spans of vector sets that are not present in Mathlib.

theorem span_eq_of_maximal_subset_linearIndepOn {α R O : Type} [DivisionRing R] [AddCommGroup O] [Module R O] {v : α → O} {s : Set α} (t : Set α) (hs : Maximal (fun (r : Set α) => r ⊆ t ∧ LinearIndepOn R v r) s) : Submodule.span R (v '' s) = Submodule.span R (v '' t)

theorem span_eq_top_of_maximal_linearIndepOn {α R O : Type} [DivisionRing R] [AddCommGroup O] [Module R O] {v : α → O} {s : Set α} (hs : Maximal (LinearIndepOn R v) s) : Submodule.span R (v '' s) = Submodule.span R v.range