Theorem ValuativeRel.isEquiv_ofValuation

Modification history

2026-10-19 10:34

Mathlib/RingTheory/Valuation/ValuativeRel/Basic.lean

feat(RingTheory/Valuation/ValuativeRel/Basic): add IsEquiv lemmas (#43683)

Added ValuativeRel.isEquiv_ofValuation View on Github →