Commit 2024-07-30 16:56 db8dc843

View on Github →

feat: Monotonicity of multiplication by positive rationals (#15328) From LeanAPAP

Estimated changes

added theorem abs_nnqsmul
added theorem abs_qsmul