Theorem ValuativeRel.srel_iff

Modification history

2025-10-06 16:30

Mathlib/RingTheory/Valuation/ValuativeRel/Basic.lean

feat(RingTheory/Valuation/ValuativeRel): strict valuative relation (#30262) …

Added ValuativeRel.srel_iff View on Github →