mathlib3

93219fb7 - feat(number_theory): degree `[Frac(S):Frac(R)]` is degree `[S/pS:R/p]` (#15315)

feat(number_theory): degree `[Frac(S):Frac(R)]` is degree `[S/pS:R/p]` (#15315) (for a Dedekind domain `R` and its integral closure `S` and maximal ideal `p`) This is the first step in showing the fundamental identity of inertia degree and ramification index (#12287). The next step is to factor `pS` into coprime factors `P` and use the Chinese remainder theorem. Co-authored-by: Anne Baanen <Vierkantor@users.noreply.github.com> Co-authored-by: Anne Baanen <t.baanen@vu.nl>