Commit 2026-08-03 13:47 8d2ab698

View on Github →

refactor(RingTheory/DedekindDomain): make IsDedekindDomainInv private (#42392) Make IsDedekindDomainInv private, because is the same as IsDedekindDomain. See Zulip.

Estimated changes

Modified Mathlib/RingTheory/DedekindDomain/Ideal/Basic.lean

modified theorem FractionalIdeal.adjoinIntegral_eq_one_of_isUnit

deleted theorem IsDedekindDomainInv.isDedekindDomain

modified def IsDedekindDomainInv

modified theorem isDedekindDomainInv_iff