noncomputable def GLnBuilding.frameOfBasis (k : Type u_1) [Field k] (n : ℕ) (b : Module.Basis (Fin n) k (Vec k n)) : Frame k n

Convert a basis $b$ of $k^n$ into a frame by taking lines $L_i = k \cdot b_i$.

theorem GLnBuilding.frameOfBasis_lines (k : Type u_1) [Field k] (n : ℕ) (b : Module.Basis (Fin n) k (Vec k n)) (i : Fin n) : (frameOfBasis k n b).lines i = k ∙ b i

The $i$-th line of frameOfBasis b is $k \cdot b_i$, by definition.

theorem GLnBuilding.adapted_frame_of_single_subspace (k : Type u_1) [Field k] (n : ℕ) (V : Submodule k (Vec k n)) (_hbot : V ≠ ⊥) (_htop : V ≠ ⊤) : ∃ (F : Frame k n), Frame.IsCompatible k n F V

Any proper non-zero subspace $V \subseteq k^n$ admits an adapted frame: there exists a frame $F$ for which $V = \bigoplus_{i \in S} L_i$ for some $S \subseteq \mathrm{Fin}\ n$, constructed by extending a basis of $V$ by a basis of a complement.