mathlib

25b1b1ba - feat(number_theory): the class number is finite if there is an admissible absolute value