mathlib3

4291be5d - Make `euclidean_absolute_value` a predicate on absolute values

Make `euclidean_absolute_value` a predicate on absolute values I still need the predicate to be a structure since it will be extended to `is_admissible` in the finiteness proof of the class number.