Theorem List.minimum_le_coe_iff

Modification history

2023-07-30 03:44

Mathlib/Data/List/MinMax.lean

feat(List/MinMax): maximum_of_length_pos (#6115)

Modified List.minimum_le_coe_iff View on Github →

2023-07-13 09:29

Mathlib/Data/List/MinMax.lean

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

Added List.minimum_le_coe_iff View on Github →