Commit 2023-01-27 20:59 06a8409a

View on Github →

feat: Port/Data.Finsupp.Order (#1891) port of data.finsupp.order needs explicit naming of instances in Data.Finsupp.Order.Defs

Estimated changes

Modified Mathlib.lean

Modified Mathlib/Data/Finsupp/Defs.lean

Created Mathlib/Data/Finsupp/Order.lean

added theorem Finsupp.add_eq_zero_iff

added theorem Finsupp.add_sub_single_one

added theorem Finsupp.coe_tsub

added theorem Finsupp.inf_apply

added theorem Finsupp.le_def

added theorem Finsupp.le_iff'

added theorem Finsupp.le_iff

added theorem Finsupp.monotone_toFun

added def Finsupp.orderEmbeddingToFun

added theorem Finsupp.orderEmbeddingToFun_apply

added theorem Finsupp.single_le_iff

added theorem Finsupp.single_tsub

added theorem Finsupp.sub_single_one_add

added theorem Finsupp.subset_support_tsub

added theorem Finsupp.sup_apply

added theorem Finsupp.support_inf

added theorem Finsupp.support_sup

added theorem Finsupp.support_tsub

added theorem Finsupp.tsub_apply