Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-12-27 16:46 ca2c3443

View on Github →

split(data/finsupp/order): Split off data.finsupp.basic (#11045) This moves all order instances about finsupp from data.finsupp.basic and data.finsupp.lattice to a new file data.finsupp.order. I'm crediting

Estimated changes

deleted theorem finsupp.add_eq_zero_iff
deleted theorem finsupp.coe_tsub
deleted theorem finsupp.le_def
deleted theorem finsupp.le_iff'
deleted theorem finsupp.le_iff
deleted theorem finsupp.lt_wf
deleted theorem finsupp.single_le_iff
deleted theorem finsupp.single_tsub
deleted theorem finsupp.sum_id_lt_of_lt
deleted theorem finsupp.support_tsub
deleted theorem finsupp.tsub_apply
deleted theorem finsupp.bot_eq_zero
deleted theorem finsupp.disjoint_iff
deleted theorem finsupp.inf_apply
deleted theorem finsupp.monotone_to_fun
deleted theorem finsupp.sup_apply
deleted theorem finsupp.support_inf
deleted theorem finsupp.support_sup
added theorem finsupp.coe_tsub
added theorem finsupp.disjoint_iff
added theorem finsupp.inf_apply
added theorem finsupp.le_def
added theorem finsupp.le_iff'
added theorem finsupp.le_iff
added theorem finsupp.lt_wf
added theorem finsupp.single_le_iff
added theorem finsupp.single_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