Commit 2023-08-12 20:56 80b3e90f
View on Github →refactor: make IsDedekindDomain extend the other classes (#5834)
This redefines the IsDedekindDomain class to be the conjunction through extends of the classes IsDomain, IsNoetherianRing, DimensionLEOne and IsIntegrallyClosed.
Zulip thread: https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/Should.20.60IsDedekindDomain.60.20extend.20.60IsDomain.60.3F