Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2020-04-25 23:03 ba4dc1a4

View on Github →

doc(algebra/order_functions): add docstring and lemma (#2526) I added a missing lemma, and then figured that while I was here I should add a docstring

Estimated changes