Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-09-11 12:23 241ee9ee

View on Github →

feat(data/finsupp): more lemmas about α →₀ ℕ (#9137)

Estimated changes

Modified src/data/finsupp/basic.lean

added theorem finsupp.le_iff'

added theorem finsupp.nat_add_sub_assoc

added theorem finsupp.nat_sub_self

added theorem finsupp.single_le_iff