Commit 2025-03-31 12:58 c6530632

View on Github →

feat(Data/List/MinMax): add le_max_of_le' (#23204)

Estimated changes

Modified Mathlib/Data/List/MinMax.lean

added theorem List.le_max_of_le'

added theorem List.min_le_of_le'