Theorem ValuativeExtension.veq_iff_veq

Modification history

2026-10-27 23:51
Mathlib/RingTheory/Valuation/ValuativeRel/Basic.lean
feat: valuative extensions preserve `=ᵥ` relation (#45320) …
Added ValuativeExtension.veq_iff_veqView on Github →