Theorem Finsupp.monotone_toFun

Modification history

2023-12-07 11:12
Mathlib/Data/Finsupp/Order.lean
feat: When `Finsupp.prod` is nonzero (#8844) …
Deleted Finsupp.monotone_toFunView on Github →
2023-01-27 20:59
Mathlib/Data/Finsupp/Order.lean
feat: Port/Data.Finsupp.Order (#1891) …
Added Finsupp.monotone_toFunView on Github →