Commit 2023-09-19 10:04 2c07b501
View on Github →feat: IsDedekindRing is IsDedekindDomain minus IsDomain (#6127)
This PR defines IsDedekindRing as IsDedekindDomain without the bundled IsDomain hypothesis.
Zulip thread: https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/Should.20.60IsDedekindDomain.60.20extend.20.60IsDomain.60.3F