[math-fun] mixed orthogonal groups