Commit 2021-09-02 08:19 9d3e3e8a

feat(ring_theory/dedekind_domain): the integral closure of a DD is a DD (#8847) Let L be a finite separable extension of K = Frac(A), where A is a Dedekind domain. Then any is_integral_closure C A L is also a Dedekind domain, in particular for C := integral_closure A L. In combination with the definitions of #8701, we can conclude that rings of integers are Dedekind domains.