Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-10-06 21:14 f63786b9

View on Github →

refactor(data/finsupp/basic): has_ordered_sub on finsupp (#9577)

  • Generalize has_sub and canonically_ordered_add_monoid instances for any finsupp with codomain a canonically_ordered_add_monoid & has_ordered_sub.
  • Provide has_ordered_sub instance in the same situation
  • Generalize lemmas about nat to this situation.
  • Prove some lemmas as special cases of has_ordered_sub lemmas. These will be removed in a subsequent PR.
  • Simplify some lemmas about α →₀ ℕ using has_ordered_sub lemmas.
  • Prove nat.one_le_iff_ne_zero (it's the second time I want to use it this week)

Estimated changes

modified theorem finsupp.coe_nat_sub
modified theorem finsupp.nat_add_sub_assoc
modified theorem finsupp.nat_add_sub_cancel
modified theorem finsupp.nat_add_sub_of_le
modified theorem finsupp.nat_sub_add_cancel
modified theorem finsupp.nat_sub_apply
modified theorem finsupp.nat_sub_self
modified theorem finsupp.nat_zero_sub
modified theorem finsupp.single_nat_sub
added theorem nat.one_le_iff_ne_zero