Commit 2023-09-14 10:14 433091dd
View on Github →refactor: remove IsDomain hypothesis from IsIntegrallyClosed (#6126)
This PR modifies the definition of IsIntegrallyClosed to drop the IsDomain hypothesis. This change came out of the discussions of modifying IsDedekindDomain to either extend IsDomain or to drop IsDomain entirely and change it to IsDedekindRing. (The former being a dependency of this PR, the latter a follow-up.)
Zulip thread: https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/Should.20.60IsDedekindDomain.60.20extend.20.60IsDomain.60.3F