Theorem DFinsupp.coe_orderEmbeddingToFun

Modification history

2024-01-17 23:23
Mathlib/Data/DFinsupp/Order.lean
chore(*): rename `FunLike` to `DFunLike` (#9785) …
Modified DFinsupp.coe_orderEmbeddingToFunView on Github →
2023-12-07 11:12
Mathlib/Data/DFinsupp/Order.lean
feat: When `Finsupp.prod` is nonzero (#8844) …
Added DFinsupp.coe_orderEmbeddingToFunView on Github →