noncomputable def
GLnBuilding.twoChamberFrameHyp
(k : Type u_1)
[Field k]
(n : ℕ)
(h : SimultaneousRefinementHyp k n)
:
Given the simultaneous refinement hypothesis, two chambers $\sigma, \tau$ admit a common adapted frame, obtained by applying the refinement to the concatenated chain.