noncomputable def IsometryBuilding.isometryIsBuilding_wired {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) : IsBuilding B n

Concrete wiring: produces the isometry building from a hyperbolic frame, by plugging in the common-apartment and apartment-exchange instances.