Commit 2025-11-22 20:23 b07a5845

View on Github →

chore: rename mul_le_mul_right' to mul_le_mul_left (#30242)

Estimated changes

Modified Archive/Wiedijk100Theorems/CubingACube.lean

Modified Counterexamples/OrderedCancelAddCommMonoidWithBounds.lean

Modified Mathlib/Algebra/Algebra/Operations.lean

Modified Mathlib/Algebra/Group/UniqueProds/Basic.lean

Modified Mathlib/Algebra/Lie/Subalgebra.lean

Modified Mathlib/Algebra/Module/Submodule/Pointwise.lean

Modified Mathlib/Algebra/MonoidAlgebra/Degree.lean

Modified Mathlib/Algebra/Order/AbsoluteValue/Basic.lean

Modified Mathlib/Algebra/Order/AddTorsor.lean

Modified Mathlib/Algebra/Order/BigOperators/Group/List.lean

Modified Mathlib/Algebra/Order/Field/Pi.lean

Modified Mathlib/Algebra/Order/Group/Defs.lean

deleted theorem LinearOrderedCommGroup.mul_lt_mul_left'

Modified Mathlib/Algebra/Order/Group/Int.lean

Modified Mathlib/Algebra/Order/Group/Nat.lean

Modified Mathlib/Algebra/Order/Group/Opposite.lean

Modified Mathlib/Algebra/Order/Group/PiLex.lean

Modified Mathlib/Algebra/Order/Group/Units.lean

Modified Mathlib/Algebra/Order/GroupWithZero/Canonical.lean

Modified Mathlib/Algebra/Order/GroupWithZero/Unbundled/Defs.lean

Modified Mathlib/Algebra/Order/Monoid/Associated.lean

Modified Mathlib/Algebra/Order/Monoid/Canonical/Defs.lean

Modified Mathlib/Algebra/Order/Monoid/Defs.lean

Modified Mathlib/Algebra/Order/Monoid/OrderDual.lean

Modified Mathlib/Algebra/Order/Monoid/Prod.lean

Modified Mathlib/Algebra/Order/Monoid/Unbundled/Basic.lean

deleted theorem mul_le_mul_left'

added theorem mul_le_mul_left

deleted theorem mul_le_mul_right'

added theorem mul_le_mul_right

deleted theorem mul_lt_mul_left'

added theorem mul_lt_mul_left

deleted theorem mul_lt_mul_right'

added theorem mul_lt_mul_right

Modified Mathlib/Algebra/Order/Monoid/Unbundled/Units.lean

Modified Mathlib/Algebra/Order/Nonneg/Ring.lean

Modified Mathlib/Algebra/Order/Pi.lean

Modified Mathlib/Algebra/Order/Positive/Ring.lean

Modified Mathlib/Algebra/Order/Ring/Archimedean.lean

Modified Mathlib/Algebra/Order/Ring/Basic.lean

Modified Mathlib/Algebra/Order/Ring/Canonical.lean

Modified Mathlib/Algebra/Order/Ring/Nat.lean

Modified Mathlib/Algebra/Order/Ring/Rat.lean

Modified Mathlib/Algebra/Order/Star/Basic.lean

Modified Mathlib/Algebra/Order/ToIntervalMod.lean

Modified Mathlib/Algebra/Tropical/Basic.lean

Modified Mathlib/Analysis/CStarAlgebra/Multiplier.lean

Modified Mathlib/Analysis/FunctionalSpaces/SobolevInequality.lean

Modified Mathlib/Analysis/Matrix/Order.lean

Modified Mathlib/Analysis/MeanInequalities.lean

Modified Mathlib/Analysis/Normed/Group/Basic.lean

Modified Mathlib/Analysis/Normed/Module/MStructure.lean

Modified Mathlib/Analysis/Normed/Ring/Basic.lean

Modified Mathlib/Analysis/Normed/Unbundled/SeminormFromConst.lean

Modified Mathlib/Analysis/Normed/Unbundled/SmoothingSeminorm.lean

Modified Mathlib/Analysis/PSeries.lean

Modified Mathlib/Combinatorics/Additive/CauchyDavenport.lean

Modified Mathlib/Combinatorics/Additive/Energy.lean

Modified Mathlib/Combinatorics/Additive/PluenneckeRuzsa.lean

Modified Mathlib/Combinatorics/SetFamily/Kleitman.lean

Modified Mathlib/Computability/Language.lean

Modified Mathlib/Data/ENNReal/Action.lean

Modified Mathlib/Data/ENNReal/Basic.lean

Modified Mathlib/Data/ENNReal/Inv.lean

Modified Mathlib/Data/ENNReal/Operations.lean

deleted theorem ENNReal.mul_le_mul_left

deleted theorem ENNReal.mul_le_mul_right

deleted theorem ENNReal.mul_lt_mul_left

deleted theorem ENNReal.mul_lt_mul_right

Modified Mathlib/Data/EReal/Inv.lean

Modified Mathlib/Data/Finsupp/Lex.lean

Modified Mathlib/Data/Int/Interval.lean

Modified Mathlib/Data/Nat/Choose/Factorization.lean

Modified Mathlib/Data/Nat/Fib/Zeckendorf.lean

Modified Mathlib/Data/Nat/PartENat.lean

Modified Mathlib/Data/Num/ZNum.lean

Modified Mathlib/Data/Ordmap/Ordset.lean

Modified Mathlib/Data/Real/Basic.lean

Modified Mathlib/Data/Real/StarOrdered.lean

Modified Mathlib/Geometry/Convex/Cone/Basic.lean

Modified Mathlib/GroupTheory/DivisibleHull.lean

Modified Mathlib/GroupTheory/MonoidLocalization/Order.lean

Modified Mathlib/GroupTheory/Schreier.lean

Modified Mathlib/LinearAlgebra/AffineSpace/FiniteDimensional.lean

Modified Mathlib/MeasureTheory/Covering/Besicovitch.lean

Modified Mathlib/MeasureTheory/Covering/BesicovitchVectorSpace.lean

Modified Mathlib/MeasureTheory/Covering/Differentiation.lean

Modified Mathlib/MeasureTheory/Function/Intersectivity.lean

Modified Mathlib/MeasureTheory/Function/Jacobian.lean

Modified Mathlib/MeasureTheory/Function/LpSeminorm/ChebyshevMarkov.lean

Modified Mathlib/MeasureTheory/Function/SimpleFunc.lean

Modified Mathlib/MeasureTheory/Group/GeometryOfNumbers.lean

Modified Mathlib/MeasureTheory/Integral/Bochner/VitaliCaratheodory.lean

Modified Mathlib/MeasureTheory/Integral/Lebesgue/Add.lean

Modified Mathlib/MeasureTheory/Integral/MeanInequalities.lean

Modified Mathlib/NumberTheory/EllipticDivisibilitySequence.lean

Modified Mathlib/NumberTheory/FrobeniusNumber.lean

Modified Mathlib/NumberTheory/Zsqrtd/Basic.lean

Modified Mathlib/Order/Filter/ENNReal.lean

Modified Mathlib/Order/Partition/Equipartition.lean

Modified Mathlib/Probability/Independence/Integration.lean

Modified Mathlib/Probability/Kernel/Defs.lean

Modified Mathlib/RingTheory/DedekindDomain/Different.lean

Modified Mathlib/RingTheory/DedekindDomain/Factorization.lean

Modified Mathlib/RingTheory/FractionalIdeal/Basic.lean

Modified Mathlib/RingTheory/HahnSeries/Lex.lean

Modified Mathlib/RingTheory/KrullDimension/Regular.lean

Modified Mathlib/RingTheory/MvPowerSeries/Order.lean

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

Modified Mathlib/SetTheory/Cardinal/Arithmetic.lean

Modified Mathlib/SetTheory/Cardinal/Divisibility.lean

Modified Mathlib/SetTheory/Cardinal/Order.lean

Modified Mathlib/SetTheory/Cardinal/Regular.lean

Modified Mathlib/SetTheory/Game/Basic.lean

Modified Mathlib/SetTheory/Ordinal/Arithmetic.lean

Modified Mathlib/SetTheory/Ordinal/Basic.lean

Modified Mathlib/SetTheory/Ordinal/Exponential.lean

Modified Mathlib/SetTheory/Ordinal/FixedPoint.lean

Modified Mathlib/SetTheory/Ordinal/NaturalOps.lean

added theorem Ordinal.nmul_le_nmul

modified theorem Ordinal.nmul_le_nmul_left

modified theorem Ordinal.nmul_le_nmul_right

Modified Mathlib/SetTheory/Ordinal/Notation.lean

Modified Mathlib/SetTheory/Ordinal/Principal.lean

Modified Mathlib/SetTheory/PGame/Algebra.lean

modified theorem SetTheory.PGame.le_iff_sub_nonneg

modified theorem SetTheory.PGame.lt_iff_sub_pos

Modified Mathlib/SetTheory/Surreal/Basic.lean

Modified Mathlib/Tactic/LinearCombination/Lemmas.lean

Modified Mathlib/Tactic/Ring/Compare.lean

added theorem Mathlib.Tactic.Ring.add_le_add_left

deleted theorem Mathlib.Tactic.Ring.add_le_add_right

added theorem Mathlib.Tactic.Ring.add_lt_add_left

deleted theorem Mathlib.Tactic.Ring.add_lt_add_right

Modified Mathlib/Topology/ContinuousMap/CompactlySupported.lean

Modified Mathlib/Topology/ContinuousMap/Ideals.lean

Modified Mathlib/Topology/ContinuousMap/Lattice.lean

Modified Mathlib/Topology/EMetricSpace/Lipschitz.lean

Modified Mathlib/Topology/EMetricSpace/PairReduction.lean

Modified Mathlib/Topology/Instances/ENNReal/Lemmas.lean

Modified Mathlib/Topology/MetricSpace/Dilation.lean

Modified Mathlib/Topology/MetricSpace/Holder.lean

Modified MathlibTest/ValuedCSP.lean