Empty_Set_is_Linearly_Independent
Provedlinear-algebralinear-independenceproofwiki
The empty set is a linearly independent set.
Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem Empty_Set_is_Linearly_Independent {R : Type _} [Ring R] {M : Type _} [AddCommGroup M] [Module R M] : LinearIndependent R (fun (x : (∅ : Set M)) => (x : M)) := by sorrySource