Commit 2026-01-18 12:47 277a145e

View on Github →

refactor(RingTheory/Valuation/ValuativeRel/Basic): fix theorem names for multiplication (#33658) We rename vle_mul_right to mul_vle_mul_left and reorder its arguments to match mul_le_mul_left, and other analogous changes.

Estimated changes

Modified Mathlib/RingTheory/Valuation/ValuativeRel/Basic.lean

modified theorem ValuativeRel.mul_vle_mul

added theorem ValuativeRel.mul_vle_mul_right

modified theorem ValuativeRel.one_vlt_inv

modified theorem ValuativeRel.vle_mul_left

deleted theorem ValuativeRel.vle_mul_left_iff

added theorem ValuativeRel.vle_mul_right

deleted theorem ValuativeRel.vle_mul_right_iff

deleted theorem ValuativeRel.vlt_mul_left_iff

deleted theorem ValuativeRel.vlt_mul_right_iff

Modified Mathlib/RingTheory/Valuation/ValuativeRel/Trivial.lean