[Merged by Bors] - chore(RingTheory/Ideal/Norm/RelNorm): switch over to new definitions of ramificationIdx and inertiaDeg#41077

tb65536 wants to merge 5 commits into

leanprover-community:masterleanprover-community/mathlib4:masterfrom

tb65536:tb_ref04793tb65536/mathlib4:tb_ref04793Copy head branch name to clipboard