[proofplan] We compute the valuation of the different $\mathfrak{D}_{L/K}$ by expressing it as the ideal generated by $f'(\pi_L)$, where $f$ is the minimal polynomial of a uniformizer $\pi_L$ of $L$ over $K$. We then evaluate $v_L(f'(\pi_L))$ by factoring $f'$ using the roots of $f$ (the conjugates of $\pi_L$) and relating the valuations of the differences $\pi_L - \sigma(\pi_L)$ to the ramification function $i_{L/K}(\sigma)$. Summing over all non-identity elements of $G$ yields the formula $v_L(\mathfrak{D}_{L/K}) = \sum_{s=0}^{\infty}(|G_s| - 1)$. [/proofplan] [step:Express the different via the minimal polynomial of a uniformizer] Since $L/K$ is a finite Galois extension of local fields, $L/K$ is separable and $\mathcal{O}_L = \mathcal{O}_K[\pi_L]$ for any uniformizer $\pi_L$ of $L$ (this follows because $\{1, \pi_L, \ldots, \pi_L^{n-1}\}$ is an $\mathcal{O}_K$-basis of $\mathcal{O}_L$, where $n = [L:K]$, since the residue extensions and ramification account for the full degree). Let $f(x) \in \mathcal{O}_K[x]$ be the minimal polynomial of $\pi_L$ over $K$, which has degree $n$. By the formula for the different of a monogenic extension: \begin{align*} \mathfrak{D}_{L/K} = (f'(\pi_L)), \end{align*} so $v_L(\mathfrak{D}_{L/K}) = v_L(f'(\pi_L))$. [guided] Why is $\mathcal{O}_L = \mathcal{O}_K[\pi_L]$? For a finite extension of local fields, if $\pi_L$ is a uniformizer of $L$, then $L = K(\pi_L)$ (since $1, \pi_L, \ldots, \pi_L^{e-1}$ give representatives for $e$ distinct residue classes of $\mathfrak{m}_L/\mathfrak{m}_L^2$, combined with lifts of a $k_L/k_K$ basis). The ring $\mathcal{O}_K[\pi_L]$ is a free $\mathcal{O}_K$-module of rank $n = [L:K]$ with basis $\{1, \pi_L, \ldots, \pi_L^{n-1}\}$, and it is contained in $\mathcal{O}_L$. Since $\mathcal{O}_L$ is also a free $\mathcal{O}_K$-module of rank $n$, the inclusion $\mathcal{O}_K[\pi_L] \subseteq \mathcal{O}_L$ of free modules of equal rank over a PID means $\mathcal{O}_L/\mathcal{O}_K[\pi_L]$ is a finite torsion module. For local fields, one can verify the discriminant of $\{1, \pi_L, \ldots, \pi_L^{n-1}\}$ generates the same ideal as the discriminant of any $\mathcal{O}_K$-basis of $\mathcal{O}_L$, giving $\mathcal{O}_L = \mathcal{O}_K[\pi_L]$. The formula $\mathfrak{D}_{L/K} = (f'(\pi_L))$ is a standard result for monogenic extensions: when $\mathcal{O}_L = \mathcal{O}_K[\alpha]$ with minimal polynomial $f$, the different ideal equals $(f'(\alpha))$. [/guided] [/step] [step:Factor $f'(\pi_L)$ using the Galois conjugates] Since $f$ is the minimal polynomial of $\pi_L$ over $K$ and $L/K$ is Galois, the roots of $f$ in $L$ are precisely $\{\sigma(\pi_L) : \sigma \in G\}$ where $G = \operatorname{Gal}(L/K)$. Thus: \begin{align*} f(x) = \prod_{\sigma \in G}(x - \sigma(\pi_L)). \end{align*} Taking the derivative: \begin{align*} f'(x) = \sum_{\tau \in G} \prod_{\substack{\sigma \in G \\ \sigma \neq \tau}} (x - \sigma(\pi_L)). \end{align*} Evaluating at $x = \pi_L$: for $\tau \neq \operatorname{id}$, the product $\prod_{\sigma \neq \tau}(\pi_L - \sigma(\pi_L))$ contains the factor $\pi_L - \operatorname{id}(\pi_L) = 0$ (from the $\sigma = \operatorname{id}$ term). So only the $\tau = \operatorname{id}$ term survives: \begin{align*} f'(\pi_L) = \prod_{\substack{\sigma \in G \\ \sigma \neq \operatorname{id}}} (\pi_L - \sigma(\pi_L)). \end{align*} [/step] [step:Compute $v_L(f'(\pi_L))$ using the ramification function] Applying $v_L$ to the product: \begin{align*} v_L(f'(\pi_L)) = \sum_{\substack{\sigma \in G \\ \sigma \neq \operatorname{id}}} v_L(\pi_L - \sigma(\pi_L)). \end{align*} By definition of the ramification function, $i_{L/K}(\sigma) = v_L(\sigma(\pi_L) - \pi_L)$ for $\sigma \neq \operatorname{id}$. Since $v_L(\pi_L - \sigma(\pi_L)) = v_L(\sigma(\pi_L) - \pi_L)$ (the valuation is insensitive to sign), we have: \begin{align*} v_L(\mathfrak{D}_{L/K}) = \sum_{\substack{\sigma \in G \\ \sigma \neq \operatorname{id}}} i_{L/K}(\sigma). \end{align*} [guided] The ramification function $i_{L/K}: G \to \mathbb{Z}_{\geq -1} \cup \{\infty\}$ is defined by $i_{L/K}(\operatorname{id}) = \infty$ and $i_{L/K}(\sigma) = v_L(\sigma(\pi_L) - \pi_L)$ for $\sigma \neq \operatorname{id}$. This is independent of the choice of uniformizer $\pi_L$. The key property is that $\sigma \in G_s$ (the $s$-th lower ramification group) if and only if $i_{L/K}(\sigma) \geq s + 1$. [/guided] [/step] [step:Rewrite the sum as $\sum_{s=0}^{\infty}(|G_s| - 1)$] We rearrange the sum by interchanging the order of summation. For each $\sigma \neq \operatorname{id}$, write $i_{L/K}(\sigma) = \sum_{s=0}^{i_{L/K}(\sigma)-1} 1$. Then: \begin{align*} \sum_{\substack{\sigma \in G \\ \sigma \neq \operatorname{id}}} i_{L/K}(\sigma) = \sum_{\substack{\sigma \in G \\ \sigma \neq \operatorname{id}}} \sum_{s=0}^{i_{L/K}(\sigma)-1} 1 = \sum_{s=0}^{\infty} \left|\{\sigma \in G \setminus \{\operatorname{id}\} : i_{L/K}(\sigma) \geq s + 1\}\right|. \end{align*} By definition of the lower ramification groups, $G_s = \{\sigma \in G : i_{L/K}(\sigma) \geq s + 1\}$. Therefore: \begin{align*} \left|\{\sigma \in G \setminus \{\operatorname{id}\} : i_{L/K}(\sigma) \geq s + 1\}\right| = |G_s| - 1, \end{align*} since $\operatorname{id} \in G_s$ for all $s$ (as $i_{L/K}(\operatorname{id}) = \infty$). Substituting: \begin{align*} v_L(\mathfrak{D}_{L/K}) = \sum_{s=0}^{\infty} (|G_s| - 1). \end{align*} The sum is finite because $G_s = \{\operatorname{id}\}$ for all sufficiently large $s$ (since $i_{L/K}(\sigma)$ is finite for $\sigma \neq \operatorname{id}$), so $|G_s| - 1 = 0$ for large $s$. [guided] The interchange of summation is a standard Fubini-type argument for non-negative sums. We write the double sum as counting pairs $(s, \sigma)$ with $\sigma \neq \operatorname{id}$ and $0 \leq s \leq i_{L/K}(\sigma) - 1$. Fixing $s$ first and summing over $\sigma$ gives exactly $|G_s| - 1$ (all elements of $G_s$ except the identity). Why is the identity always in $G_s$? Because $i_{L/K}(\operatorname{id}) = \infty \geq s + 1$ for every $s \geq 0$. Why is the sum finite? For $\sigma \neq \operatorname{id}$, the value $i_{L/K}(\sigma) = v_L(\sigma(\pi_L) - \pi_L)$ is a finite non-negative integer. Let $M = \max_{\sigma \neq \operatorname{id}} i_{L/K}(\sigma)$. Then for $s \geq M$, $G_s = \{\operatorname{id}\}$ and $|G_s| - 1 = 0$. [/guided] [/step]