\begin{definition}[Definition:Index of Subgroup/Finite]
Let $G$ be a group.
Let $H$ be a subgroup of $G$.
Let $\index G H$ denote the index of $H$ in $G$, that is, the cardinality of the left (or right) coset space $G / H$.
If $G / H$ is a finite set, then $\index G H$ is '''finite''', and $H$ is '''of finite index''' in $G$.
\end{definition}