[proofplan] We use the [Equivalent Characterisations of Galois Extensions](/theorems/3310) to reduce to the fact that $K$ is the splitting field of a separable polynomial $f \in k[x]$. The proof then proceeds by induction on $[K : k]$. In the inductive step, we adjoin a single root $\alpha$ of $f$ to $k$, count the $k$-automorphisms of $K$ that fix $\alpha$ (which form $\operatorname{Gal}(K/k(\alpha))$), and then count the possible images of $\alpha$ under an arbitrary $k$-automorphism. The [Tower Law](/theorems/1248) and the multiplicativity of these counts yield $|\operatorname{Gal}(K/k)| = [K : k]$. [/proofplan] [step:Reduce to the splitting field of a separable polynomial] Since $K/k$ is Galois, the [Equivalent Characterisations of Galois Extensions](/theorems/3310) gives that $K/k$ is both normal and separable, and that $K$ is the splitting field of some separable polynomial $f \in k[x]$ over $k$. We prove the result by strong induction on $n = [K : k]$. [guided] What does it mean for $K/k$ to be Galois? By the [Equivalent Characterisations of Galois Extensions](/theorems/3310), a finite extension $K/k$ is Galois if and only if it is both normal and separable, which in turn is equivalent to $K$ being the splitting field of a separable polynomial $f \in k[x]$. This characterisation is the right starting point because it gives us a concrete polynomial whose roots generate $K$, and we can count automorphisms by tracking where those roots go. We proceed by strong induction on the degree $n = [K : k]$. [/guided] [/step] [step:Establish the base case $[K : k] = 1$] If $[K : k] = 1$, then $K = k$ and the only $k$-automorphism of $K$ is the identity. Hence $|\operatorname{Gal}(K/k)| = 1 = [K : k]$. [guided] The base case is $n = [K : k] = 1$. This forces $K = k$ as vector spaces over $k$, so every element of $K$ already lies in $k$. A $k$-automorphism must fix $k$ pointwise, and since $K = k$, the only such map is the identity $\operatorname{id}_K$. Hence $|\operatorname{Gal}(K/k)| = 1 = [K : k]$. [/guided] [/step] [step:Pick a root $\alpha$ of $f$ not in $k$ and identify the minimal polynomial] Suppose $[K : k] = n > 1$. Since $K \neq k$, the polynomial $f$ has an irreducible factor $p \in k[x]$ of degree $d := \deg p \geq 2$. Let $\alpha \in K$ be a root of $p$. Since $f$ is separable over $k$, the irreducible factor $p$ is separable, so $p$ has $d$ distinct roots $\alpha = \alpha_1, \alpha_2, \ldots, \alpha_d$ in $K$. The minimal polynomial of $\alpha$ over $k$ is $p$, so $[k(\alpha) : k] = d$. [guided] Since $[K : k] > 1$, the field $K$ is strictly larger than $k$. The polynomial $f$ has at least one irreducible factor $p \in k[x]$ of degree $d \geq 2$ (if all factors were linear, then all roots of $f$ would lie in $k$, and the splitting field would be $k$ itself, contradicting $K \neq k$). Let $\alpha \in K$ be a root of $p$. Because $f$ is separable over $k$, its irreducible factor $p$ is also separable: $p$ has no repeated roots in $K$. Denote the $d$ distinct roots of $p$ in $K$ by $\alpha_1 = \alpha, \alpha_2, \ldots, \alpha_d$. Since $p$ is irreducible over $k$ and $p(\alpha) = 0$, the polynomial $p$ is the minimal polynomial of $\alpha$ over $k$, and $[k(\alpha) : k] = d$. [/guided] [/step] [step:Apply the inductive hypothesis to $K/k(\alpha)$] The extension $K/k(\alpha)$ is the splitting field of $f$ over $k(\alpha)$ (since $K$ is generated over $k$ by the roots of $f$, and those same roots generate $K$ over $k(\alpha)$). The polynomial $f$ remains separable over $k(\alpha)$ because separability depends only on having distinct roots. By the [Equivalent Characterisations of Galois Extensions](/theorems/3310), $K/k(\alpha)$ is Galois. By the [Tower Law](/theorems/1248), \begin{align*} [K : k(\alpha)] = \frac{[K : k]}{[k(\alpha) : k]} = \frac{n}{d} < n, \end{align*} since $d \geq 2$. By the inductive hypothesis, \begin{align*} |\operatorname{Gal}(K/k(\alpha))| = [K : k(\alpha)] = \frac{n}{d}. \end{align*} [guided] We now examine the intermediate extension $k \subset k(\alpha) \subset K$. The field $K$ is generated over $k$ by the roots of $f$; those same roots lie in $K$ and generate $K$ over the larger field $k(\alpha)$ as well. Hence $K$ is the splitting field of $f$ over $k(\alpha)$. Separability is a property of the polynomial (having distinct roots in its splitting field), so $f$ is still separable over $k(\alpha)$. By the [Equivalent Characterisations of Galois Extensions](/theorems/3310), $K/k(\alpha)$ is Galois. By the [Tower Law](/theorems/1248), $[K : k] = [K : k(\alpha)] \cdot [k(\alpha) : k]$, so $[K : k(\alpha)] = n/d$. Since $d \geq 2$, we have $n/d < n$, so the inductive hypothesis applies and gives $|\operatorname{Gal}(K/k(\alpha))| = n/d$. The group $\operatorname{Gal}(K/k(\alpha))$ consists of those $k$-automorphisms of $K$ that additionally fix $\alpha$. This will be important in the next step, where we count all $k$-automorphisms of $K$ by partitioning them according to where they send $\alpha$. [/guided] [/step] [step:Partition $\operatorname{Gal}(K/k)$ according to the image of $\alpha$] Let $\sigma \in \operatorname{Gal}(K/k)$. Since $\sigma$ fixes $k$ pointwise and $p(\alpha) = 0$, we have $p(\sigma(\alpha)) = \sigma(p(\alpha)) = 0$, so $\sigma(\alpha)$ is a root of $p$ in $K$. Hence $\sigma(\alpha) \in \{\alpha_1, \ldots, \alpha_d\}$. For each $1 \leq j \leq d$, define \begin{align*} S_j := \{\sigma \in \operatorname{Gal}(K/k) : \sigma(\alpha) = \alpha_j\}. \end{align*} These sets partition $\operatorname{Gal}(K/k)$, and $S_1 = \operatorname{Gal}(K/k(\alpha))$. [guided] Every $k$-automorphism $\sigma$ of $K$ must permute the roots of any polynomial over $k$: if $p(\alpha) = 0$ and $p$ has coefficients in $k$, then applying $\sigma$ to $p(\alpha) = 0$ gives $p(\sigma(\alpha)) = 0$ because $\sigma$ fixes each coefficient of $p$. So $\sigma(\alpha)$ is one of the $d$ roots $\alpha_1, \ldots, \alpha_d$ of $p$. This observation gives a natural partition of $\operatorname{Gal}(K/k)$: for each root $\alpha_j$, collect all automorphisms sending $\alpha \mapsto \alpha_j$ into a fibre $S_j$. Every automorphism belongs to exactly one fibre (it sends $\alpha$ to exactly one root), so $\operatorname{Gal}(K/k) = S_1 \sqcup S_2 \sqcup \cdots \sqcup S_d$. The fibre $S_1$ consists of those automorphisms fixing $\alpha$, which is precisely $\operatorname{Gal}(K/k(\alpha))$. If we can show that all $d$ fibres have the same size, then $|\operatorname{Gal}(K/k)| = d \cdot |S_1| = d \cdot (n/d) = n$, and the induction closes. [/guided] [/step] [step:Show each fibre $S_j$ is non-empty and has the same size as $\operatorname{Gal}(K/k(\alpha))$] [claim:Each $S_j$ is non-empty and $|S_j| = |\operatorname{Gal}(K/k(\alpha))|$] Since $K/k$ is normal and $p$ is irreducible over $k$, all roots $\alpha_j$ of $p$ lie in $K$. By the [Extension of Isomorphisms to Splitting Fields](/theorems/3313) applied to the $k$-isomorphism $k(\alpha) \cong k(\alpha_j)$ sending $\alpha \mapsto \alpha_j$ (which exists because $\alpha$ and $\alpha_j$ have the same minimal polynomial $p$ over $k$), this isomorphism extends to a $k$-automorphism $\tau_j: K \to K$. Hence $\tau_j \in S_j$, so $S_j \neq \varnothing$. The map \begin{align*} S_1 &\to S_j \\ \sigma &\mapsto \tau_j \circ \sigma \end{align*} is a bijection, with inverse $\sigma \mapsto \tau_j^{-1} \circ \sigma$. Indeed, for $\sigma \in S_1$, we have $\sigma(\alpha) = \alpha$, so $(\tau_j \circ \sigma)(\alpha) = \tau_j(\alpha) = \alpha_j$, hence $\tau_j \circ \sigma \in S_j$. Conversely, for $\sigma \in S_j$, we have $(\tau_j^{-1} \circ \sigma)(\alpha) = \tau_j^{-1}(\alpha_j) = \alpha$, so $\tau_j^{-1} \circ \sigma \in S_1$. Therefore $|S_j| = |S_1| = |\operatorname{Gal}(K/k(\alpha))|$. [/claim] [guided] We need two things: that each fibre $S_j$ is non-empty, and that all fibres have the same cardinality. **Non-emptiness.** Since $K/k$ is normal, every irreducible polynomial over $k$ that has one root in $K$ splits completely in $K$. In particular, all $d$ roots $\alpha_1, \ldots, \alpha_d$ of $p$ lie in $K$. Now, $\alpha$ and $\alpha_j$ share the same minimal polynomial $p$ over $k$, so the evaluation map $\alpha \mapsto \alpha_j$ extends to a $k$-isomorphism $k(\alpha) \cong k(\alpha_j)$. By the [Extension of Isomorphisms to Splitting Fields](/theorems/3313), this $k$-isomorphism extends to a $k$-automorphism $\tau_j: K \to K$ of the splitting field. Since $\tau_j(\alpha) = \alpha_j$, we have $\tau_j \in S_j$, so $S_j \neq \varnothing$. **Equal cardinality.** We exhibit an explicit bijection $S_1 \to S_j$. Define the map $\sigma \mapsto \tau_j \circ \sigma$. Why does this land in $S_j$? If $\sigma \in S_1 = \operatorname{Gal}(K/k(\alpha))$, then $\sigma(\alpha) = \alpha$, so $(\tau_j \circ \sigma)(\alpha) = \tau_j(\alpha) = \alpha_j$, confirming $\tau_j \circ \sigma \in S_j$. The inverse map is $\sigma \mapsto \tau_j^{-1} \circ \sigma$: for $\sigma \in S_j$, we have $\sigma(\alpha) = \alpha_j$, so $(\tau_j^{-1} \circ \sigma)(\alpha) = \tau_j^{-1}(\alpha_j) = \alpha$, hence $\tau_j^{-1} \circ \sigma \in S_1$. These maps are mutually inverse, so $|S_j| = |S_1| = |\operatorname{Gal}(K/k(\alpha))|$. Geometrically, each $S_j$ is a left coset $\tau_j \cdot \operatorname{Gal}(K/k(\alpha))$ of the subgroup $\operatorname{Gal}(K/k(\alpha)) \le \operatorname{Gal}(K/k)$, and cosets of a subgroup always have the same cardinality. [/guided] [/step] [step:Combine the counts to conclude $|\operatorname{Gal}(K/k)| = [K : k]$] Since $\operatorname{Gal}(K/k) = S_1 \sqcup S_2 \sqcup \cdots \sqcup S_d$ is a disjoint partition with $|S_j| = |\operatorname{Gal}(K/k(\alpha))| = n/d$ for each $j$, we obtain \begin{align*} |\operatorname{Gal}(K/k)| = d \cdot \frac{n}{d} = n = [K : k]. \end{align*} This completes the induction and the proof. [guided] We have partitioned $\operatorname{Gal}(K/k)$ into $d$ cosets $S_1, \ldots, S_d$, each of size $|\operatorname{Gal}(K/k(\alpha))| = n/d$. Summing: \begin{align*} |\operatorname{Gal}(K/k)| = \sum_{j=1}^{d} |S_j| = d \cdot \frac{n}{d} = n = [K : k]. \end{align*} This is a multiplicative counting argument: there are $d$ choices for where $\alpha$ can be sent (one for each root of its minimal polynomial), and for each such choice, there are $n/d$ automorphisms that extend it (by the inductive hypothesis applied to the smaller Galois extension $K/k(\alpha)$). The total count is $d \cdot (n/d) = n$. Note that this argument simultaneously proves the upper bound (each automorphism must send $\alpha$ to a root of $p$, giving at most $d$ fibres) and the lower bound (every fibre is non-empty by the extension theorem). The induction closes because $[K : k(\alpha)] = n/d < n$ whenever $d \geq 2$. [/guided] [/step]