Def ValuativeRel.veq

Modification history

2026-01-21 07:32

Mathlib/RingTheory/Valuation/ValuativeRel/Basic.lean

feat(RingTheory/Valuation/ValuativeRel): introduce `=ᵥ` relation (#33532) …

Added ValuativeRel.veq View on Github →