Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-02-26 10:06 ff5fa529

View on Github →

chore(data/finsupp/basic): add coe_{neg,sub,smul} lemmas to match coe_{zero,add,fn_sum} (#6350) This also:

  • merges together smul_apply' and smul_apply, since the latter is just a special case of the former.
  • changes the implicitness of arguments to all of the finsupp.*_apply lemmas so that all the variables and none of the types are explicit The whitespace style here matches how coe_add is spaced.

Estimated changes

modified theorem finsupp.add_apply
modified def finsupp.apply_add_hom
added theorem finsupp.coe_nat_sub
added theorem finsupp.coe_neg
added theorem finsupp.coe_smul
added theorem finsupp.coe_sub
modified theorem finsupp.nat_sub_apply
modified theorem finsupp.neg_apply
deleted theorem finsupp.smul_apply'
modified theorem finsupp.smul_apply
modified theorem finsupp.sub_apply
modified def is_basis.coord_fun