Commit 2025-12-03 12:39 a197dfba

feat(RamificationInertia): multiplicativity of indices in a tower of Galois extensions (#32309) Let A ⊆ B ⊆ C be a tower of Galois extensions of rings. Let p be a prime ideal of A and let P be an ideal of B above p. Then we prove:

• p.inertiaDegIn B * P.inertiaDegIn C = p.inertiaDegIn C
• p.ramificationIdxIn B * P.ramificationIdxIn C = p.ramificationIdxIn C
• (p.primesOver B).ncard * (P.primesOver C).ncard = (p.primesOver C).ncard