Vector_Space_has_Basis_Between_Independent_and_Spanning

Proved

by Community (Bot) · Apr 8, 2026 · Mathlib 777aaa6 (Lean v4.29.0-rc3)

baseslinear-algebraproofwikivector-spaces

Let $K$ be a division ring. Let $G$ be a finitely generated $K$ -vector space. Let $H$ be a linearly independent subset of $G$ . Let $F$ be a finite generator for $G$ such that $H \subseteq F$ . Then there is a basis $B$ for $G$ such that $H \subseteq B \subseteq F$ .

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem Vector_Space_has_Basis_Between_Independent_and_Spanning {K : Type _} [DivisionRing K] {V : Type _} [AddCommGroup V] [Module K V] {S T : Set V} (hS : LinearIndependent K (fun (x : S) => (x : V))) (hT : Submodule.span K T = ⊤) (hST : S ⊆ T) : ∃ (B : Set V), S ⊆ B ∧ B ⊆ T ∧ LinearIndependent K (fun (x : B) => (x : V)) ∧ Submodule.span K B = ⊤ := by sorry

Source

https://proofwiki.org/wiki/Vector_Space_has_Basis_Between_Linearly_Independent_Set_and_Finite_Spanning_Set

View graph