mathlib3
9eefd40e - refactor(data/list/min_max): use with_top for maximum and define argmax (#1320)

Commit
6 years ago
refactor(data/list/min_max): use with_top for maximum and define argmax (#1320) * refactor(data/list/min_max): use option for maximum and define argmax * prove minimum_singleton * fix build * use with_bot for maximum * update comments
Author
Committer
Parents
Loading