feat(number_theory): define the class number (#9071)
We instantiate the finiteness proof of the class group for rings of integers, and define the class number of a number field, or of a separable function field, as the finite cardinality of the class group.
Co-Authored-By: Ashvni <ashvni.n@gmail.com>
Co-Authored-By: Filippo A. E. Nuccio <filippo.nuccio@univ-st-etienne.fr>
Co-authored-by: Johan Commelin <johan@commelin.net>
Co-authored-by: Anne Baanen <Vierkantor@users.noreply.github.com>
