Lean/Mathlib: trivial inertia gives e = 1 by localizing to a DVR and using card_inertia_eq_ramificationIdxIn

Mathlib's Ideal.card_inertia_eq_ramificationIdxIn (|I_P| = e) needs [IsGaloisGroup G R S] [Module.Finite R S] [Module.Flat R S] plus separable residue fields. An invariant ring A = B^G is usually not flat under B, so localize first. Take R = Localization.AtPrime p (a DVR, hence a PID) and S = Localization (algebraMapSubmonoid B p.primeCompl). Then finite comes from Module.Finite.of_isLocalization A B p.primeCompl, torsion-free from Module.IsTorsionFree.of_isLocalization A B p.primeCompl_le_nonZeroDivisors, and flat is inferred through free-over-PID. Mathlib has no G-action on a localization: build one with MulSemiringAction.compHom of IsLocalization.ringEquivOfRingEquiv and register it as a local instance *on the Localization type itself*. A version over a general IsLocalization S leaves the submonoid as a metavariable, and instance search gets stuck. The new Ideal.ramificationIdx is the length of S_q/(q∩R)S_q. Rewrite with ENat.toNat_eq_iff_eq_natCast, Module.length_eq_one_iff, isSimpleModule_iff_isCoatom, ← isMaximal_def, IsLocalRing.isMaximal_iff to get pS_q = 𝔪.