This is a repo on which I am planning (as soon as I find some time to organise it!) to store some of the code I wrote in Lean during summer 2021 to prove the Dedekind-Kummer theorem.
Most of what I wrote have already made its way into mathlib :
- Results about sums of ideals in Dedekind domains,
- Results about quotients of polynomial rings,
- Results about successive quotients of rings : here and here,
- Results about UFDs,*
- Results about multisets : here and here,
- Results about quotients of various structures : here and here.
- Results about divisibility,
- Results about UFDs,*
- Results about Dedekind domains.
- Results about order theory
- [...]
- The Dedekind-Kummer Theorem in the monogenic case
- Basic theory of conductor ideals - all the stuff that's needed for the general version of the Dedekind-Kummer Theorem
*To be more precise these results are proved in the more general setting of Unique Factorisation Monoids.