Theorem IsIntegralClosure.isDedekindDomain

Modification history

2023-08-12 20:56
Mathlib/RingTheory/DedekindDomain/IntegralClosure.lean
refactor: make IsDedekindDomain extend the other classes (#5834) …
Modified IsIntegralClosure.isDedekindDomainView on Github →
2023-06-20 23:35
Mathlib/RingTheory/DedekindDomain/IntegralClosure.lean
feat: port RingTheory.DedekindDomain.IntegralClosure (#5304)
Added IsIntegralClosure.isDedekindDomainView on Github →