Commit 2026-02-19 10:30 90c2e6ba

View on Github →

feat(RingTheory/Valuation/Basic): generalize lemmas from DivisionRing to Ring (#35479)

Estimated changes

Modified Mathlib/RingTheory/Valuation/Basic.lean

modified theorem Valuation.isEquiv_iff_val_lt_val

modified theorem Valuation.isEquiv_map_self_of_strictMono