mathlib3

585a1bf3 - feat(number_theory): define ramification index and inertia degree (#14332)

feat(number_theory): define ramification index and inertia degree (#14332) We define ramification index `ramification_idx` and inertia degree `inertia_deg` for `P : ideal S` over `p : ideal R` given a ring extension `f : R →+* S`. The literature generally assumes `p` is included in `P`, both are maximal, `R` is the ring of integers of a number field `K` and `S` is the integral closure of `R` in `L`, a finite separable extension of `K`; we relax these assumptions as much as is practical.