[proofplan] The proof treats the two directions of the biconditional separately, with Artin's Lemma as the central tool in both. For the forward direction, we assume $L/K$ is Galois, set $H = \operatorname{Aut}_K(L)$, and use the equality $|H| = [L:K]$ together with Artin's Lemma to show that $[L:L^H] = |H| = [L:K]$; since $K \subset L^H \subset L$, the tower law forces $L^H = K$. For the converse, we assume $L^{\operatorname{Aut}_K(L)} = K$, set $H = \operatorname{Aut}_K(L)$, and invoke Artin's Lemma to conclude that $L/L^H = L/K$ is a finite Galois extension with $\operatorname{Gal}(L/K) = H$. [/proofplan] [step:Forward direction: assume $L/K$ is Galois and show $L^{\operatorname{Aut}_K(L)} = K$] Set $H = \operatorname{Aut}_K(L)$. Since $L/K$ is a finite Galois extension, $H = \operatorname{Gal}(L/K)$ and $|H| = [L : K]$. Every element of $H$ fixes $K$ pointwise, so $K \subset L^H$. We show that no element outside $K$ is fixed by all of $H$. By [Artin's Lemma](/theorems/1272), applied to the finite group $H \subset \operatorname{Aut}(L)$, the extension $L/L^H$ is finite with $[L : L^H] = |H|$. Since $K \subset L^H \subset L$, the tower law gives \begin{align*} [L : K] = [L : L^H] \cdot [L^H : K]. \end{align*} Substituting $[L : L^H] = |H| = [L : K]$: \begin{align*} [L : K] = [L : K] \cdot [L^H : K], \end{align*} which forces $[L^H : K] = 1$. Therefore $L^H = K$, i.e., $L^{\operatorname{Aut}_K(L)} = K$. [guided] We want to show that if $L/K$ is Galois, then the only elements of $L$ fixed by every $K$-automorphism are the elements of $K$ itself. The strategy is to use a degree-counting argument: Artin's Lemma pins down $[L : L^H]$, and the tower law then forces $L^H$ to equal $K$. Set $H = \operatorname{Aut}_K(L)$. Since $L/K$ is a finite Galois extension (finite, separable, and normal), we have $H = \operatorname{Gal}(L/K)$ and the fundamental equality $|H| = [L : K]$. Every $\sigma \in H$ satisfies $\sigma(a) = a$ for all $a \in K$ (since $\sigma$ is a $K$-automorphism), so $K \subset L^H$. The question is whether $L^H$ could be strictly larger than $K$ — that is, whether there might exist elements outside $K$ that are nonetheless fixed by every automorphism. The degree argument shows this cannot happen. We apply [Artin's Lemma](/theorems/1272). The hypotheses require $H$ to be a finite subgroup of $\operatorname{Aut}(L)$. We verify: $H = \operatorname{Gal}(L/K)$ is finite (with $|H| = [L:K] < \infty$), and every element of $H$ is a field automorphism of $L$. Artin's Lemma therefore gives $[L : L^H] = |H|$. Now, $K \subset L^H \subset L$ is a tower of field extensions, so multiplicativity of degrees applies: \begin{align*} [L : K] = [L : L^H] \cdot [L^H : K]. \end{align*} We have $[L : L^H] = |H| = [L : K]$. Substituting: \begin{align*} [L : K] = [L : K] \cdot [L^H : K]. \end{align*} Since $[L : K]$ is a positive integer (it is finite and nonzero), we may divide both sides by $[L : K]$ to obtain $[L^H : K] = 1$. An extension of degree $1$ is an equality of fields, so $L^H = K$. This is the content of the forward direction: the Galois group of a Galois extension is "large enough" ($|H| = [L:K]$) to ensure that no element outside $K$ escapes being moved by some automorphism. If $|H|$ were strictly smaller than $[L:K]$ — as happens for non-Galois extensions — then $L^H$ would be strictly larger than $K$, and some elements would be "invisible" to the automorphism group. [/guided] [/step] [step:Converse direction: assume $L^{\operatorname{Aut}_K(L)} = K$ and show $L/K$ is Galois] Set $H = \operatorname{Aut}_K(L)$. Since $L/K$ is a finite extension, $H$ is a finite group: every $K$-automorphism of $L$ permutes the roots of the minimal polynomial of each element of $L$ over $K$, and there are finitely many such roots, so $|H| \le [L:K]! < \infty$. (In fact, $|H| \le [L:K]$, but the weaker bound suffices here.) By hypothesis, $L^H = K$. We apply [Artin's Lemma](/theorems/1272) to the finite group $H \subset \operatorname{Aut}(L)$. The conclusion is: 1. $L/L^H$ is a finite Galois extension. 2. $\operatorname{Gal}(L/L^H) = H$. 3. $[L : L^H] = |H|$. Since $L^H = K$, statement (1) gives that $L/K$ is a finite Galois extension, which is the desired conclusion. Moreover, $\operatorname{Gal}(L/K) = H = \operatorname{Aut}_K(L)$ by statement (2), and $[L:K] = |H|$ by statement (3). [guided] We now prove the converse: if $L/K$ is a finite extension satisfying $L^{\operatorname{Aut}_K(L)} = K$, then $L/K$ is Galois. Set $H = \operatorname{Aut}_K(L)$, the group of all $K$-automorphisms of $L$. We first verify that $H$ is finite. Each $\sigma \in H$ is a $K$-automorphism of $L$, so $\sigma$ is determined by its values on any $K$-basis of $L$. More precisely, if $\alpha \in L$ is any element, then $\sigma(\alpha)$ must be a root of $\operatorname{min}_K(\alpha) \in K[x]$, and $\operatorname{min}_K(\alpha)$ has at most $\deg(\operatorname{min}_K(\alpha)) \le [L:K]$ roots. Since $L/K$ is finite, $L$ is finitely generated as a $K$-algebra, and a $K$-automorphism is determined by its action on a finite generating set. This gives $|H| < \infty$. We now apply [Artin's Lemma](/theorems/1272) to the finite group $H \subset \operatorname{Aut}(L)$. The hypotheses of Artin's Lemma require that $H$ is a finite subgroup of $\operatorname{Aut}(L)$. We have verified finiteness, and every element of $H$ is by definition a field automorphism of $L$. Artin's Lemma therefore yields three conclusions: 1. $L/L^H$ is a finite Galois extension. 2. $\operatorname{Gal}(L/L^H) = H$. 3. $[L : L^H] = |H|$. The hypothesis $L^H = K$ transforms these into: 1. $L/K$ is a finite Galois extension. 2. $\operatorname{Gal}(L/K) = H = \operatorname{Aut}_K(L)$. 3. $[L : K] = |H| = |\operatorname{Aut}_K(L)|$. Statement (1) is the desired conclusion. The logic of this direction deserves emphasis: the assumption $L^{\operatorname{Aut}_K(L)} = K$ says that the automorphism group, whatever its size, is "large enough relative to $K$" in the sense that no element of $L \setminus K$ is fixed by all automorphisms. Artin's Lemma converts this fixed-field condition into a structural conclusion — the extension $L/L^H$ is automatically separable and normal. The hypothesis $L^H = K$ then transports this structural conclusion down to $L/K$. Note that the finiteness of $L/K$ is essential in both directions. Without it, $H = \operatorname{Aut}_K(L)$ need not be finite, and Artin's Lemma (which requires a finite group of automorphisms) would not apply. For instance, $\overline{\mathbb{Q}}/\mathbb{Q}$ satisfies $\overline{\mathbb{Q}}^{\operatorname{Aut}_\mathbb{Q}(\overline{\mathbb{Q}})} = \mathbb{Q}$, and it is Galois, but the proof mechanism is different — one passes through finite sub-extensions and takes a direct limit. [/guided] [/step] [step:Combine both directions to complete the biconditional] The forward direction (Step 1) shows: if $L/K$ is a finite Galois extension, then $L^{\operatorname{Aut}_K(L)} = K$. The converse direction (Step 2) shows: if $L/K$ is a finite extension with $L^{\operatorname{Aut}_K(L)} = K$, then $L/K$ is Galois. Together, these establish that a finite extension $L/K$ is Galois if and only if $L^{\operatorname{Aut}_K(L)} = K$. [/step]