Commit 2025-08-13 11:43 aacdbd89

View on Github →

chore(Algebra/Order): replace Co/ContravariantClass by established abbrevs (#28239) ... Add/MulLeft/Right(Strict)Mono and Add/MulLeft/RightReflectLE

Estimated changes

Modified Mathlib/Algebra/BigOperators/Group/Multiset/Basic.lean

Modified Mathlib/Algebra/MonoidAlgebra/Degree.lean

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

modified theorem le_mul_of_forall_lt

modified theorem mul_le_of_forall_lt

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

modified theorem max_mul

modified theorem min_mul

modified theorem mul_max

modified theorem mul_min

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

modified theorem WithBot.addLECancellable_coe

modified theorem WithBot.addLECancellable_of_lt_bot

modified theorem WithBot.addLECancellable_of_ne_bot

modified theorem WithTop.addLECancellable_coe

modified theorem WithTop.addLECancellable_of_lt_top

modified theorem WithTop.addLECancellable_of_ne_top

Modified Mathlib/Data/DFinsupp/Order.lean

Modified Mathlib/Data/Finsupp/Order.lean

Modified Mathlib/Order/Filter/IsBounded.lean

Modified Mathlib/Probability/Kernel/Defs.lean

Modified Mathlib/Topology/Algebra/Order/LiminfLimsup.lean