Submodule Spans

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

theorem in_submoduleSpan_range {α : Type u_1} {R : Type u_2} {O : Type u_3} [AddCommGroup O] [Semiring R] [Module R O] (f : α → O) (a : α) : f a ∈ Submodule.span R f.range

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

theorem span_eq_top_of_maximal_linearIndepOn {α : Type u_1} {R : Type u_2} {O : Type u_3} [AddCommGroup O] [DivisionRing R] [Module R O] {f : α → O} {s : Set α} (hf : Maximal (LinearIndepOn R f) s) : Submodule.span R (f '' s) = Submodule.span R f.range