mathlib3

359173d3 - feat(number_theory/class_number): define "admissible" absolute values