theorem GLnBuilding.strictMono_nat_id {n : ℕ} (g : Fin (n + 1) → ℕ) (hg : StrictMono g) (_h0 : g ⟨0, ⋯⟩ = 0) (hn : g ⟨n, ⋯⟩ = n) (j : Fin (n + 1)) : g j = ↑j

A strictly monotone map $g : \mathrm{Fin}(n+1) \to \mathbb{N}$ with $g(0) = 0$ and $g(n) = n$ must be the identity.

theorem GLnBuilding.linearIndependent_of_not_mem_span_predecessors {k : Type u_1} [Field k] {V : Type u_2} [AddCommGroup V] [Module k V] {m : ℕ} (v : Fin m → V) (h : ∀ (j : Fin m), v j ∉ Submodule.span k (v '' {i : Fin m | ↑i < ↑j})) : LinearIndependent k v

If no vector in a finite family is in the span of its predecessors (under the natural ordering of Fin m), then the family is linearly independent.

noncomputable def GLnBuilding.basisFromFlagHyp (k : Type u_2) [Field k] (n : ℕ) : BasisFromFlagHyp k n

Proof of BasisFromFlagHyp: from any maximal proper flag $0 \subsetneq V_1 \subsetneq \cdots \subsetneq V_{n-1} \subsetneq k^n$, extract $n$ lines $L_i$ that decompose $k^n$ as $k^n = L_1 \oplus \cdots \oplus L_n$ and such that each $V_j$ is a join of some subset of the $L_i$ — i.e.\ extract an adapted basis.