mathlib3

d0259b01 - refactor(ring_theory/class_group): redefine class_group without fraction field (#16727)

refactor(ring_theory/class_group): redefine class_group without fraction field (#16727) Although the definition of the class group of a ring `R` involves the field of fractions, the definition does not depend (up to isomorphism) on the choice of field of fractions. This PR proposes to always choose `fraction_ring R` as that field, so that we don't need to carry around the mathematically unnecessary parameters `(K) [field K] [algebra R K] [is_fraction_ring R K]`. Instead, we insert the isomorphism between the definitions of class group at the API boundaries. This was inspired by our work on quadratic rings: it gets even more annoying when you need to start carrying around a proof that the field of fractions of `ℤ[1/2√-7]` is `ℚ(√-7)`. Co-authored-by: Anne Baanen <t.baanen@vu.nl> Co-authored-by: Anne Baanen <Vierkantor@users.noreply.github.com>