mathlib3

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