mathlib

4c60258c - chore(ring_theory/dedekind_domain/ideal): golf (#12737)