Auxiliary file: c_eq_zero_iff—tameness as the vanishing of c (p.1031)

The paper states that c L = 0 exactly when n is prime to the residue characteristic p, in other words when L / K is tamely ramified ([Serre 1978, p.1031][Serre1978]). Both directions come from the same coefficient-by-coefficient valuation bookkeeping at an Eisenstein generator, with no different ideal and no tame classification:

• p ∤ n implies c L = 0—the residue of n is then nonzero, so n is a unit of 𝒪[K] (addVal_natCast_eq_zero), and the uniform bound of the finiteness half of Remark 1° (c_le_of_mem_sigma) reads c L ≤ 0 at t = 0, the valuation of n being zero.
• p ∣ n implies c L ≠ 0 (n_le_d_of_dvd)—every coefficient of the derivative of g at ξ, the sum of the terms i * a i * ξ ^ (i - 1), is divisible by the uniformizer: the Eisenstein coefficients below the top lie in 𝓂[K] by definition, and the top one is n itself, which p ∣ n puts in 𝓂[K] (dvd_natCast_of_dvd). Every term of the power-basis combination then has valuation at least n, so orthogonality (le_addVal_sum_iff) gives n ≤ d L, d L being the valuation of that derivative (addVal_derivative_eq_d); hence 1 ≤ c L, as c L = d L + 1 - n.

Classically this is the characterization of tame ramification by d = e - 1 ([Serre 1979, Chap. III, §6, Prop. 13][Serre1979]).

References

• [Serre1978] J-P. Serre, Une «formule de masse» pour les extensions totalement ramifiées de degré donné d'un corps local, C. R. Acad. Sci. Paris 286 (1978), Série A, 1031–1036.
• [Serre1979] J-P. Serre, Local fields, Graduate Texts in Mathematics 67, Springer, 1979.

theorem MassFormula.c_eq_zero_iff (K : Type u_1) [Field K] [ValuativeRel K] [UniformSpace K] [IsNonarchimedeanLocalField K] (n : ℕ) (hn : 0 < n) (L : IntermediateField K (SeparableClosure K)) (hL : L ∈ sigma K n) : c L = 0 ↔ ¬ringChar (IsLocalRing.ResidueField ↥(ValuativeRel.valuation K).integer) ∣ n

c L = 0 if and only if n is prime to the residue characteristic, in other words if and only if L / K is tamely ramified, assembled from the two bounds above ([Serre 1978, p.1031][Serre1978]).