Commit 2023-07-13 09:29 228477b0

View on Github →

feat: add minimum_le_coe_iff for List.minimum (#5845)

Estimated changes

Modified Mathlib/Data/List/MinMax.lean

added theorem List.coe_le_maximum_iff

added theorem List.minimum_le_coe_iff