Commit 2025-02-28 14:11 7b186b76

View on Github →

feat(Data/List): List.maximum_append (#22398) also proves the minimum counterpart

Estimated changes

Modified Mathlib/Data/List/MinMax.lean

added theorem List.maximum_append

added theorem List.minimum_append