Commit 2023-10-27 10:36 7a2492cd

View on Github →

add minimum_of_length_pos_mem (#7974) add minimum_of_length_pos_mem to Mathlib/Data/List

Estimated changes

Modified Mathlib/Data/List/MinMax.lean

added theorem List.maximum_of_length_pos_mem

added theorem List.minimum_of_length_pos_mem