Commit 2023-04-20 07:06 cdc34484
View on Github →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.