Theorem Valuation.IsEquiv.compatible

Modification history

2026-09-25 16:01
Mathlib/RingTheory/Valuation/ValuativeRel/Basic.lean
feat(Valued/ValuationTopology): creating instances of `IsValuativeTopology` on completion (#36769) …
Added Valuation.IsEquiv.compatibleView on Github →