mathlib3

d4ab959a - feat(number_theory): the ring of integers is a Dedekind domain