mathlib

86db394f - feat(number_theory): fundamental identity of ramification index and inertia degree (#12287)

feat(number_theory): fundamental identity of ramification index and inertia degree (#12287) This PR proves the fundamental identity of ramification index and inertia degree: Let `p` be a prime in a Dedekind domain `R`, `S` the integral closure of `R` in some finite field extension `L` of `K = Frac(R)`, then for `P` ranging over the primes lying over `p`, `Σ P, e P * f P = [L : K]`. Co-authored-by: Anne Baanen <Vierkantor@users.noreply.github.com>