Theorem. “$[K : K^{G}] = \\lvert G \\rvert$” [2301]

Let $K / F$ be a finite field extension and $G \leq \mathrm{Aut}(K / F)$. Then $[K : K^{G}] = \lvert G \rvert$.