Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2019-11-18 16:16 0d94020c

View on Github →

feat(algebra/order_functions): define min/max_mul_of_nonneg (#1698) Also define monotone_mul_right_of_nonneg and rename monotone_mul_of_nonneg to monotone_mul_left_of_nonneg.

Estimated changes

added theorem max_mul_of_nonneg
added theorem min_mul_of_nonneg
deleted theorem monotone_mul_of_nonneg