Commit 2025-04-23 12:17 e218a97a
View on Github →chore(RingTheory/DedekindDomain): fix namespace inconsistency (#24313)
We have some lemmas in the namespace IsDedekindDomain and others in DedekindDomain. Standardize on the Is version (and remove some redundant variable re-declarations).