mathlib

cdc34484 - refactor(algebra/module/dedekind_domain): eliminate existentials (#14734)

refactor(algebra/module/dedekind_domain): eliminate existentials (#14734) This extracts some constructions from some long existentials so that we don't have to prove everything about the construction in a single place. This makes some of the statements longer, so in places the existential version is kept in terms of the definition one.