Superset_of_Linearly_Dependent_Set
Provedlinear-algebralinear-independenceproofwiki
Any set containing a linearly dependent set is also linearly dependent.
Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem Superset_of_Linearly_Dependent_Set {R : Type _} [Ring R] {M : Type _} [AddCommGroup M] [Module R M] {S T : Set M} (hST : S ⊆ T) (hS : ¬ LinearIndependent R (fun (x : S) => (x : M))) : ¬ LinearIndependent R (fun (x : T) => (x : M)) := by sorrySource