Theorem ValuativeRel.not_vlt_of_veq

Modification history

2026-01-21 07:32
Mathlib/RingTheory/Valuation/ValuativeRel/Basic.lean
feat(RingTheory/Valuation/ValuativeRel): introduce `=ᵥ` relation (#33532) …
Added ValuativeRel.not_vlt_of_veqView on Github →