mathlib

813725f8 - feat(number_theory/kummer_dedekind): define conductor and add basic API plus theorem (#16833)

feat(number_theory/kummer_dedekind): define conductor and add basic API plus theorem (#16833) In this PR we define the conductor ideal and prove some basic results about it. In a later PR (#16870), these will be used to prove the Dedekind-Kummer theorem in full generality. Co-authored-by: Paul Lezeau <paul.lezeau@gmail.com>