Def ValuativeRel.srel

Modification history

2025-11-17 13:13

Mathlib/RingTheory/Valuation/ValuativeRel/Basic.lean

feat(RingTheory): API for valuative rel (#30423)

Deleted ValuativeRel.srel View on Github →

2025-10-06 16:30

Mathlib/RingTheory/Valuation/ValuativeRel/Basic.lean

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

Added ValuativeRel.srel View on Github →