Commit 2026-10-11 10:17 59113005
View on Github →fix(Data/DFinsupp,Order/Preorder/Finsupp): make coe_strictMono state StrictMono (#44705)
DFinsupp.coe_strictMono and Finsupp.coe_strictMono stated Monotone: upgrade their conclusion to StrictMono (which needs no proof changes).
Neither is used elsewhere in Mathlib.