Commit 2025-06-24 23:05 1b03e7b1

View on Github →

feat(Algebra/Order): more general version of abs_qsmul (#26179) This generalize abs_qsmul to any module with linearly ordered coefficient ring & PosSMulMono.

Estimated changes

added theorem abs_smul
modified theorem abs_qsmul