Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-09-28 14:01 15f15a6e

View on Github →

chore(order/*): replace mono_incr and mono_decr in lemma names wih monotone and antitone (#9428) This change was performed as a find-and-replace. No occurrences of incr or decr appear as tokens in lemma names after this change.

Estimated changes