Commit 2025-07-10 14:00 1cc889e0

View on Github →

feat(RingTheory/Valuation/Discrete/Basic.lean): add Nontriviality instances for discrete valuations (#26587) Co-authored by: María Inés de Frutos Fernández @mariainesdff

Estimated changes