mathlib3

79bf30e0 - feat(number_theory/class_number): define "admissible" absolute values