 Orthogonal group as a regular level set

The smooth Gram map $F(A)=A^{T}A$ takes real matrices to symmetric matrices. At an orthogonal $A$, its derivative sends $AH/2$ to any prescribed symmetric matrix $H$. The regular level set $F^{-1}(I)$ is therefore a smooth manifold of the displayed dimension.

// Target: geometry-and-topology.bigb