Proposition. necessary and sufficient conditions for finite $K / F$ to be Galois [22013]

A finite extension $K / F$ is Galois if and only if $\lvert \mathrm{Aut}(K / F) \rvert = [K : F]$.

Proof. sketch [22013A]

$\implies$: Since $K / F$ is Galois, it is normal and separable. By (2) of Proposition 2207, $\lvert \mathrm{Aut}(K / F) \rvert = \# \{ F\text{-embeddings }\varphi : K \to \overline{F} \}$. By Proposition 1707, $\#\{ F\text{-embeddings }\varphi : K \to \overline{F} \} = [K : F]$. Hence $\lvert \mathrm{Aut}(K / F) \rvert = [K : F]$.

$\impliedby$: By (2) of Proposition 2207, $\lvert \mathrm{Aut}(K / F)\rvert = [K : F] \leq \# \{ F\text{-embeddings }\varphi : K \to \overline{F} \}$. By Proposition 1707, $[K : F] \geq \#\{ F\text{-embeddings }\varphi : K \to \overline{F} \}$. Hence $[K : F] = \#\{ F\text{-embeddings }\varphi : K \to \overline{F} \} \implies$ $K / F$ is separable. At the same time, $\lvert \mathrm{Aut}(K / F) \rvert = \#\{ F\text{-embeddings }\varphi : K \to \overline{F} \} \implies$ $K / F$ is normal. Therefore, $K / F$ is Galois.