noncomputable def GLnBuilding.glnIsBuilding_unconditional (k : Type u_1) [Field k] (n : ℕ) : IsBuilding k n

Main theorem: the flag complex of $\mathrm{GL}_n(k)$ over any field $k$ is a building, constructed unconditionally by combining the thinness, common-apartment, and apartment-iso proofs.