Commit 2026-06-08 10:43 37166e0b
View on Github →feat(RingTheory/RamificationInertia/Inertia): inertia degree is invariant under a group action (#40124)
This PR proves that inertia degree is invariant under a group action. We already have this for the old definition inertiaDeg, but we will need this new version for inertiaDeg' for the upcoming refactor.