mathlib3

28c57ffd - feat(number_theory): the class group of an integral closure is finite

feat(number_theory): the class group of an integral closure is finite 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.