mathlib3

ea0bcd84 - feat(number_theory/class_number/finite): remove useless assumption [dedekind_domain R] (#19109)

feat(number_theory/class_number/finite): remove useless assumption [dedekind_domain R] (#19109) Remove the useless assumption `[dedekind_domain R]` from the final lemma [class_group.fintype_of_admissible_of_finite](https://leanprover-community.github.io/mathlib_docs/number_theory/class_number/finite.html#class_group.fintype_of_admissible_of_finite) since this can be inferred by the Euclidean domain one, that is in force thanks the standing assumption is that `R` has an admissible absolute value.