Commit 2021-07-30 02:40 8c89a525

feat(algebra/ordered_monoid_lemmas): add one strict_mono lemma and a few doc-strings (#8465) The product of strictly monotone functions is strictly monotone (and some doc-strings). Zulip discussion