Commit 2024-08-17 12:07 fb7b6b78

View on Github →

chore (Data.Multiset.Basic): avoid bundled ordered algebra for basic results on multisets (#14477) Data.Multiset.Basic is a fairly low-level file. Currently, it imports Algebra.Order.Monoid.Defs to establish that multisets on a type are an StrictOrderedAddCancelCommMonoid and uses that classes API in a dozen places. Unfortunately, this also adds, to this file and all that import it, the projections from the ordered monoids defined in Algebra.Order.Monoid.Defs as instances for Lean to try when synthesizing a CommMonoid impacting performance. This PR moves the ordered monoid instances to a new file Data.Multiset.OrderedMonoid and makes minor changes to Basic to avoid this import.

Estimated changes

modified theorem Finset.sum_range_tsub
deleted theorem AddHom.le_map_tsub
deleted theorem AddMonoidHom.le_map_tsub
added theorem Even.tsub
deleted theorem OrderIso.map_tsub
added theorem add_tsub_cancel_iff_le
added theorem add_tsub_eq_max
deleted theorem le_mul_tsub
deleted theorem le_tsub_mul
added theorem tsub_add_cancel_iff_le
added theorem tsub_add_eq_max
added theorem tsub_add_min
added theorem tsub_eq_tsub_min
added theorem tsub_eq_zero_iff_le
added theorem tsub_le_self
added theorem tsub_le_tsub_iff_left
added theorem tsub_lt_of_lt
added theorem tsub_lt_self
added theorem tsub_lt_self_iff
added theorem tsub_lt_tsub_iff_right
added theorem tsub_min
added theorem tsub_pos_iff_lt
added theorem tsub_pos_iff_not_le
added theorem tsub_pos_of_lt
added theorem tsub_right_inj
added theorem tsub_self
added theorem tsub_self_add
added theorem tsub_tsub_eq_min
added theorem zero_tsub
deleted theorem Even.tsub
deleted theorem add_tsub_cancel_iff_le
deleted theorem add_tsub_eq_max
deleted theorem tsub_add_cancel_iff_le
deleted theorem tsub_add_eq_max
deleted theorem tsub_add_min
deleted theorem tsub_eq_tsub_min
deleted theorem tsub_eq_zero_iff_le
deleted theorem tsub_le_self
deleted theorem tsub_le_tsub_iff_left
deleted theorem tsub_lt_of_lt
deleted theorem tsub_lt_self
deleted theorem tsub_lt_self_iff
deleted theorem tsub_lt_tsub_iff_right
deleted theorem tsub_min
deleted theorem tsub_pos_iff_lt
deleted theorem tsub_pos_iff_not_le
deleted theorem tsub_pos_of_lt
deleted theorem tsub_right_inj
deleted theorem tsub_self
deleted theorem tsub_self_add
deleted theorem tsub_tsub_eq_min
deleted theorem zero_tsub
added theorem AddHom.le_map_tsub
added theorem OrderIso.map_tsub
added theorem le_mul_tsub
added theorem le_tsub_mul
modified theorem Finset.nsmul_inf'
modified theorem Finset.nsmul_sup'