|G₀| = e for Galois Dedekind local extensions

Let $A$ be a commutative local ring which is also a Dedekind domain, and let $B$ be a commutative local ring which is a Dedekind domain, equipped with an $A$-algebra structure making $B$ a torsion-free and module-finite $A$-module. Let $G$ be a group acting on $B$ by ring automorphisms, with $G$ finite, such that IsGaloisGroup G A B holds, i.e. $G$ realises $B/A$ as a Galois extension in the sense of that predicate. Assume the maximal ideal of $B$ lies over the maximal ideal of $A$, and that the residue extension $(B/\mathfrak{m}_B)/(A/\mathfrak{m}_A)$ is separable. Assume finally $\mathfrak{m}_A \neq \bot$. Then the cardinality of the zeroth lower-numbering ramification group $G_0$ of $B$ relative to $G$ — which by definition is the inertia subgroup of $G$ attached to the ideal $\mathfrak{m}_B^{0+1} = \mathfrak{m}_B$, namely the subgroup of those $\sigma \in G$ with $\sigma(b) - b \in \mathfrak{m}_B$ for all $b \in B$ — equals $e$, the ramification index ramificationIdxIn of $\mathfrak{m}_A$ in $B$.

This is the classical identification of the order of the inertia group with the ramification index, $|G_0| = e$, in the local Galois setting with separable residue extension. It is used to convert the different-filtration formula, which is naturally expressed through $|G_0|$, into the tame statement $\mathfrak{d} = \mathfrak{m}^{e-1}$; it is cited by IsDiscreteValuationRing.addVal_coe_eq_lowerRamificationCard_zero_mul_addVal_fixedPoints.