Auxiliary file: ncard_isomorphic_mul_w—the orbit count of Remark 3°

Every L in sigma K n is isomorphic to n / w L elements of sigma K n. We express this by multiplying the cardinality of the isomorphism class by w L ([Serre 1978, Remark 3°, p.1031][Serre1978]). The count is the classical embedding argument:

• L / K is separable of degree n and SeparableClosure K is separably closed, so L has exactly n embeddings into SeparableClosure K (natCard_algHom, via Field.embEquivOfAdjoinSplits and Field.finSepDegree_eq_finrank_of_isSeparable).
• The image of an embedding stays in sigma K n (fieldRange_mem_sigma): by exists_eisenstein_generator L is generated by a root x of an Eisenstein polynomial, an embedding transports the generator with the same minimal polynomial over 𝒪[K], and isTotallyRamified_adjoin applies to the image—which is IntermediateField.adjoin K {σ x}—as it stands. No transport of integers or of the ramification data along the isomorphism is needed.
• The embeddings with a given image M are a torsor under the K-automorphisms of L: after choosing one isomorphism e M onto each member of the class, the map sending (M, g) to the composite of g, then e M, then the inclusion of M is a bijection from (class) × (automorphisms) onto the embeddings.

Taking Nat.card of the bijection gives that the number of M isomorphic to L, times w L, is n, with no finiteness bookkeeping: Nat.card is junk-0-safe on both sides, and the finiteness of the class is itself a corollary of the count.

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.

theorem MassFormula.ncard_isomorphic_mul_w (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) : {M : IntermediateField K (SeparableClosure K) | M ∈ sigma K n ∧ Nonempty (↥L ≃ₐ[K] ↥M)}.ncard * w L = n

The number of members of sigma K n that are K-isomorphic to L, times w L, is n ([Serre 1978, Remark 3°, p.1031][Serre1978]). The bijection behind the count sends a member M of the class and a K-automorphism g of L to the embedding of L into SeparableClosure K composing g, a chosen isomorphism e M onto M, and the inclusion of M; the embeddings number n (natCard_algHom), and their images all lie in the class (fieldRange_mem_sigma).