Commit 2022-11-28 16:05 84b363ae

View on Github →

feat(Algebra/Order/Monoid/MinMax): port file (#763) mathlib3 SHA: 76171581280d5b5d1e2d1f4f37e5420357bdc636 porting notes: mathport perfect modulo line breaks and an import!

Estimated changes

added theorem fn_min_mul_fn_max
added theorem lt_or_lt_of_mul_lt_mul
added theorem max_le_mul_of_one_le
added theorem max_mul_mul_left
added theorem max_mul_mul_right
added theorem min_mul_max
added theorem min_mul_mul_left
added theorem min_mul_mul_right