Commit 2021-08-18 12:08 d1b34f7b

feat(ring_theory): define the ideal class group (#8626) This PR defines the ideal class group of an integral domain, as the quotient of the invertible fractional ideals by the principal fractional ideals. It also shows that this corresponds to the more traditional definition in a Dedekind domain, namely the quotient of the nonzero ideals by I ~ J ↔ ∃ xy, xI = yJ. Co-Authored-By: Ashvni ashvni.n@gmail.com Co-Authored-By: Filippo A. E. Nuccio filippo.nuccio@univ-st-etienne.fr