mathlib

0c6f0c2a - feat(ring_theory/dedekind_domain/ideal): add lemmas about sup of ideal with irreducible (#12859)