Commit 2024-11-01 21:17 56025464
View on Github →feat(RingTheory/Valuation): PreValuationRing: without IsDomain R on the prop ValuationRing R (#17634)
This allows claiming that something is a valuation ring even before knowing that the ring is a domain, which comes up in classification of PIRs with zero divisors in the radical