Commit 2022-10-08 20:02 d0259b01

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).