mathlib icon indicating copy to clipboard operation
mathlib copied to clipboard

Published 20 hours ago • verified publisher icon leanprover-community

feat(number_theory/kummer_dedekind): define conductor and add basic API plus theorem

Open Paul-Lez opened this issue 3 years ago • 0 comments

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.

Open in Gitpod

Paul-Lez avatar Oct 06 '22 12:10 Paul-Lez