Theorem Finsupp.orderEmbeddingToFun_apply

Modification history

2023-01-27 20:59
Mathlib/Data/Finsupp/Order.lean
feat: Port/Data.Finsupp.Order (#1891) …
Added Finsupp.orderEmbeddingToFun_applyView on Github →