Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2019-03-26 18:22 8ccca3f7

View on Github →

feat(data/finsupp): add emb_domain

Estimated changes

Modified src/data/finsupp.lean

added def finsupp.emb_domain

added theorem finsupp.emb_domain_apply

added theorem finsupp.emb_domain_eq_map_domain

added theorem finsupp.emb_domain_map_range

added theorem finsupp.emb_domain_notin_range

added theorem finsupp.emb_domain_zero

added theorem finsupp.injective_map_domain

added theorem finsupp.support_emb_domain