A linearly independent set extends to a basis (Two.III.2)

Open

hefferon_linear_independent_extends_to_basis

by tianyipeng · Aug 4, 2026 · Mathlib c5ea003 (Lean v4.30.0)

basislinear-algebralinear-independence

Let $V$ be a finite-dimensional vector space over a field $K$ and let $s \subseteq V$ be linearly independent. Then $s$ is contained in some subset $t \subseteq V$ that is a basis of $V$ .

Preamble

import Definitions.Def_hefferon_prelude

open Matrix
open HefferonLinAlg

Formal statement

theorem hefferon_linear_independent_extends_to_basis
    {K V : Type*} [Field K] [AddCommGroup V] [Module K V] [FiniteDimensional K V]
    (s : Set V) (hs : LinearIndependent K ((↑) : s → V)) :
    ∃ t : Set V, s ⊆ t ∧ Nonempty (Module.Basis t K V) := by
  sorry

Source

Jim Hefferon, *Linear Algebra*, Saint Michael's College, 2020 printing, Chapter Two, Section III.2, Corollary 2.10, p. 141

View graph