mathlib

f7fc89d5 - feat(number_theory/kummer_dedekind): the return of the Dedekind-Kummer theorem. (#16870)

feat(number_theory/kummer_dedekind): the return of the Dedekind-Kummer theorem. (#16870) In this PR, we finish the proof of the general case of the Dedekind-Kummer theorem as stated in Neukirch, completing the work done in #15000. Co-authored-by: Paul Lezeau <paul.lezeau@gmail.com>