Theorem Function.isMinimalFor_argmin

Modification history

2026-08-24 11:53

Mathlib/Order/WellFounded.lean

chore(Order/WellFounded): use `to_dual` (#39438) …

Deleted Function.isMinimalFor_argmin View on Github →

2025-12-23 14:46

Mathlib/Order/WellFounded.lean

feat: connect `MinimalFor` and `Function.argmin` (#33207)

Added Function.isMinimalFor_argmin View on Github →