Lagrange's Theorem

PROP-LAG. Lagrange’s Theorem.

Let $G$ be a group and $H$ be a subgroup. Then

\[\lvert G\rvert = \lvert G/H\rvert\cdot\lvert H\rvert.\]