Theorem list.minimum_eq_coe_foldr_min_of_ne_nil
Modification history
2022-05-18 14:08
src/data/list/min_max.lean
refactor(data/list/min_max): Generalise `list.argmin`/`list.argmax` to preorders (#13221) …
Deleted list.minimum_eq_coe_foldr_min_of_ne_nilView on Github →