Theorem Finsupp.coe_tsub

Modification history

2023-12-07 11:12

Mathlib/Data/Finsupp/Order.lean

feat: When `Finsupp.prod` is nonzero (#8844) …

Modified Finsupp.coe_tsub View on Github →

2023-01-27 20:59

Mathlib/Data/Finsupp/Order.lean

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

Added Finsupp.coe_tsub View on Github →