mathlib3

9d3e3e8a - feat(ring_theory/dedekind_domain): the integral closure of a DD is a DD (#8847)

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.