mathlib3

68dbf27c - feat(number_theory): the class group of an integral closure is finite (#9059)

feat(number_theory): the class group of an integral closure is finite (#9059) This is essentially the proof that the ring of integers of a global field has a finite class group, apart from filling in each hypothesis. Co-authored-by: Anne Baanen <Vierkantor@users.noreply.github.com>