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): the return of the Dedekind-Kummer theorem.

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

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.

Open in Gitpod

Paul-Lez avatar Oct 08 '22 14:10 Paul-Lez