Commit 2025-02-18 11:27 971ebb0f

View on Github →

feat(RingTheory/Valuation/Discrete/Basic): define discrete valuations (#21371) We define (normalized) discrete valuations.

Estimated changes