Theorem Valuation.compatible_iff_isEquiv

Modification history

2026-10-19 10:34
Mathlib/RingTheory/Valuation/ValuativeRel/Basic.lean
feat(RingTheory/Valuation/ValuativeRel/Basic): add IsEquiv lemmas (#43683)
Added Valuation.compatible_iff_isEquivView on Github →