Commit 2025-02-21 11:42 2002b087

View on Github →

feat(Data/List): List.maximum is monotone (#22091) also proves the List.minimum counterpart

Estimated changes

Modified Mathlib/Data/List/MinMax.lean

added theorem List.maximum_mono

added theorem List.minimum_anti