noncomputable def
IsometryBuilding.commonIsotropicApartmentHyp
{k : Type u_1}
[CommRing k]
{V : Type u_2}
[AddCommGroup V]
[Module k V]
(B : LinearMap.BilinForm k V)
(n : ℕ)
(frame : HyperbolicFrame B n)
:
Common-apartment instance for the isometry building: a single hyperbolic frame already generates an apartment whose simplices include every isotropic chain, so any two simplices share an apartment trivially.