Commit 2025-09-21 10:40 270cdd39

View on Github →

chore: rename mul_lt_mul_left/mul_lt_mul_right to mul_lt_mul_iff_right₀/mul_lt_mul_iff_left₀ (#29295) Follow up to #28645

Estimated changes

Modified Archive/Imo/Imo2011Q3.lean

Modified Counterexamples/CanonicallyOrderedCommSemiringTwoMul.lean

deleted theorem Counterexample.Nxzmod2.mul_lt_mul_of_pos_left

deleted theorem Counterexample.Nxzmod2.mul_lt_mul_of_pos_right

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

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

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

added theorem mul_lt_mul_iff_left₀

added theorem mul_lt_mul_iff_right₀

deleted theorem mul_lt_mul_left

deleted theorem mul_lt_mul_right

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

Modified Mathlib/Algebra/Polynomial/Eval/Degree.lean

Modified Mathlib/Analysis/BoxIntegral/UnitPartition.lean

Modified Mathlib/Analysis/Convex/Slope.lean

Modified Mathlib/Analysis/Fourier/RiemannLebesgueLemma.lean

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

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

Modified Mathlib/Analysis/Real/Cardinality.lean

Modified Mathlib/Analysis/Seminorm.lean

Modified Mathlib/Analysis/SpecialFunctions/BinaryEntropy.lean

Modified Mathlib/Analysis/SpecialFunctions/Trigonometric/Arctan.lean

Modified Mathlib/Combinatorics/SimpleGraph/Regularity/Lemma.lean

Modified Mathlib/Computability/Ackermann.lean

Modified Mathlib/Data/NNReal/Defs.lean

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

Modified Mathlib/Data/Nat/Totient.lean

Modified Mathlib/Data/Ordmap/Invariants.lean

Modified Mathlib/Data/Ordmap/Ordset.lean

Modified Mathlib/Data/ZMod/ValMinAbs.lean

Modified Mathlib/FieldTheory/ChevalleyWarning.lean

Modified Mathlib/GroupTheory/Perm/Cycle/Type.lean

Modified Mathlib/MeasureTheory/Covering/Vitali.lean

Modified Mathlib/MeasureTheory/Integral/CircleIntegral.lean

Modified Mathlib/MeasureTheory/Measure/Decomposition/Lebesgue.lean

Modified Mathlib/MeasureTheory/Measure/Hausdorff.lean

Modified Mathlib/MeasureTheory/Measure/SeparableMeasure.lean

Modified Mathlib/NumberTheory/Bertrand.lean

Modified Mathlib/NumberTheory/DiophantineApproximation/Basic.lean

Modified Mathlib/SetTheory/Ordinal/Arithmetic.lean

deleted theorem Ordinal.mul_lt_mul_of_pos_left

Modified Mathlib/SetTheory/Ordinal/Exponential.lean

Modified Mathlib/SetTheory/Ordinal/FixedPoint.lean

Modified Mathlib/SetTheory/Ordinal/Notation.lean

Modified Mathlib/SetTheory/Ordinal/Principal.lean

Modified Mathlib/Tactic/Bound.lean

deleted theorem Mathlib.Tactic.Bound.mul_lt_mul_left_of_pos_of_lt

deleted theorem Mathlib.Tactic.Bound.mul_lt_mul_right_of_pos_of_lt

Modified Mathlib/Tactic/CancelDenoms/Core.lean

Modified Mathlib/Topology/Algebra/Monoid.lean

modified theorem Filter.TendstoNhdsWithinIio.const_mul

modified theorem Filter.TendstoNhdsWithinIio.mul_const

modified theorem Filter.TendstoNhdsWithinIoi.const_mul

modified theorem Filter.TendstoNhdsWithinIoi.mul_const

Modified Mathlib/Topology/MetricSpace/Contracting.lean

Modified Mathlib/Topology/MetricSpace/Dilation.lean

Modified Mathlib/Topology/MetricSpace/Lipschitz.lean