Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2020-10-20 05:38 b46190f9

View on Github →

chore(data/finsupp): minor review (#4712)

  • add a few lemmas about injectivity of coe_fn etc;
  • simplify definition of finsupp.on_finset;
  • replace the proof of support_on_finset by rfl;
  • make finsupp.mem_support_on_finset a simp lemma.

Estimated changes

added theorem finsupp.coe_mk
added theorem finsupp.coe_zero
modified theorem finsupp.ext
added theorem finsupp.ext_iff'
modified theorem finsupp.zero_apply