mathlib

0970d07d - feat(order/well_founded): define `function.argmin`, `function.argmin_on` (#8895)

feat(order/well_founded): define `function.argmin`, `function.argmin_on` (#8895) Evidently, these are just thin wrappers around `well_founded.min` but I think this use case is common enough to deserve this specialisation.