Theorem Valuation.IsEquiv.pos_iff

Modification history

2026-01-25 15:24
Mathlib/RingTheory/Valuation/Basic.lean
feat(ValuationSubring): eq_top_iff + qol changes (#33604) …
Modified Valuation.IsEquiv.pos_iffView on Github →
2025-12-05 20:44
Mathlib/RingTheory/Valuation/Basic.lean
feat: `WithVal v` and `WithVal w` are isomorphic as uniform spaces when `v` and `w` are equivalent valuations (#30133)
Added Valuation.IsEquiv.pos_iffView on Github →