Mathlib Changelog
v4
Changelog
About
Github
Commit
2025-12-23 14:46
cea71b80
View on Github →
feat: connect
MinimalFor
and
Function.argmin
(
#33207
)
Estimated changes
Modified
Mathlib/Order/WellFounded.lean
added
theorem
Function.isMinimalFor_argmin
added
theorem
Function.isMinimalFor_argminOn