Commit 2025-02-19 19:52 bcbfb20a

View on Github →

perf: turn PosMulMono and friends into classes (#22090) The only breakage is from the argument of the constructor now being implicit.

Estimated changes

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

modified theorem MulPosMono.toMulPosReflectLT

modified theorem MulPosMono.toMulPosStrictMono

modified theorem MulPosReflectLE.toMulPosStrictMono

modified theorem MulPosReflectLT.toMulPosMono

modified theorem MulPosReflectLT.toMulPosReflectLE

modified theorem PosMulMono.toPosMulReflectLT

modified theorem PosMulMono.toPosMulStrictMono

modified theorem PosMulReflectLE.toPosMulStrictMono

modified theorem PosMulReflectLT.toPosMulMono

modified theorem PosMulReflectLT.toPosMulReflectLE

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

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

Modified Mathlib/Analysis/RCLike/Basic.lean

modified theorem RCLike.instPosMulReflectLE