Free proper Lie-group action theorem (source code)

= Free proper Lie-group action theorem
{c}

If a <Lie group> acts smoothly, freely, and properly on a <smooth manifold> $P$, then the quotient $P/G$ has a unique smooth structure for which $P\to P/G$ is a <principal bundle>. An action by a compact Lie group is automatically proper.