[Merged by Bors] - feat(RingTheory/RamificationInertia/Inertia): inertia degree is invariant under a group action#40124

tb65536 wants to merge 8 commits into

leanprover-community:masterleanprover-community/mathlib4:masterfrom

tb65536:tb_inertsmultb65536/mathlib4:tb_inertsmulCopy head branch name to clipboard