feat(number_theory): Dedekind-Kummer theorem (#15000)
It's PR #15000! The Kummer-Dedekind theorem on the splitting of ideals in monogenic ring extensions.
[Zulip thread](https://leanprover.zulipchat.com/#narrow/stream/144837-PR-reviews/topic/.2315000.3A.20the.20Kummer-Dedekind.20theorem)
Co-Authored-By: Paul Lezeau <paul.lezeau@gmail.com>
Co-authored-by: Paul-Lez <72892199+Paul-Lez@users.noreply.github.com>
Co-authored-by: Johan Commelin <johan@commelin.net>
Co-authored-by: Anne Baanen <t.baanen@vu.nl>
