Theorem ValuativeRel.mul_vle_mul_right

Modification history

2026-01-18 12:47

Mathlib/RingTheory/Valuation/ValuativeRel/Basic.lean

refactor(RingTheory/Valuation/ValuativeRel/Basic): fix theorem names for multiplication (#33658) …

Added ValuativeRel.mul_vle_mul_right View on Github →