Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-08-16 16:19 e1953471

View on Github →

feat(finsupp/basic): lemmas about emb_domain (#7883)

Estimated changes

Modified src/data/finsupp/basic.lean

added def finsupp.emb_domain.add_monoid_hom

added theorem finsupp.emb_domain_add

added theorem finsupp.emb_domain_single