Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2020-02-27 11:54 a46b3e57

View on Github →

doc(data/finsupp): module docs and docstrings (#2059)

  • doc(data/finsupp): module docs and docstrings
  • chore(data/finsupp): squeeze_simp, cleanup, style
  • reviewer comments

Estimated changes

modified def finsupp.frange
modified theorem finsupp.map_domain_id
modified theorem finsupp.neg_apply
modified theorem finsupp.one_def
modified theorem finsupp.single_apply
modified theorem finsupp.single_eq_of_ne
modified theorem finsupp.single_eq_same
modified theorem finsupp.smul_apply'
added def finsupp.split
modified theorem finsupp.sub_apply
modified theorem finsupp.support_zero
modified theorem finsupp.zero_apply