Def Finsupp.orderEmbeddingToFun

Modification history

2023-02-23 12:36

Mathlib/Data/Finsupp/Order.lean

chore: tidy various files (#2462)

Modified Finsupp.orderEmbeddingToFun View on Github →

2023-01-27 20:59

Mathlib/Data/Finsupp/Order.lean

feat: Port/Data.Finsupp.Order (#1891) …

Added Finsupp.orderEmbeddingToFun View on Github →