mathlib
6c9eee4b - refactor(data/finsupp/basic): remove sub lemmas (#9603)

Commit
4 years ago
refactor(data/finsupp/basic): remove sub lemmas (#9603) * Remove the finsupp sub lemmas that are special cases of lemmas in `algebra/order/sub`, namely: * `finsupp.nat_zero_sub` * `finsupp.nat_sub_self` * `finsupp.nat_add_sub_of_le` * `finsupp.nat_sub_add_cancel` * `finsupp.nat_add_sub_cancel` * `finsupp.nat_add_sub_cancel_left` * `finsupp.nat_add_sub_assoc` * Rename the remaining lemmas to use `tsub`: * `finsupp.coe_nat_sub` → `finsupp.coe_tsub` * `finsupp.nat_sub_apply` → `finsupp.tsub_apply` Lemmas in `algebra/order/sub` will soon also use `tsub` (see [Zulip](https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/mul_lt_mul''''))
Author
Parents
Loading