Commit 2022-12-13 10:52 ca3be7d2
View on Github →feat: a * b ≤ c * d → min a b ≤ max c d (#967)
Match https://github.com/leanprover-community/mathlib/pull/17895
feat: a * b ≤ c * d → min a b ≤ max c d (#967)
Match https://github.com/leanprover-community/mathlib/pull/17895