Theorem ValuativeRel.srel_mul_left_iff

Modification history

2026-01-03 17:21
Mathlib/RingTheory/Valuation/ValuativeRel/Basic.lean
refactor: rename `≤ᵥ` to `vle` and `<ᵥ` to `vlt` (#33040) …
Deleted ValuativeRel.srel_mul_left_iffView on Github →
2025-11-17 13:13
Mathlib/RingTheory/Valuation/ValuativeRel/Basic.lean
feat(RingTheory): API for valuative rel (#30423)
Added ValuativeRel.srel_mul_left_iffView on Github →