Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-11-16 18:44 d6b83d87

View on Github →

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

Estimated changes