Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2020-10-06 10:22 372d2949

View on Github →

feat(data/finsupp): lift a collection of add_monoid_homs to an add_monoid_hom on α →₀ β (#4395)

Estimated changes

Modified src/algebra/module/basic.lean

added theorem linear_map.to_add_monoid_hom_injective

Modified src/data/finsupp/basic.lean

added theorem finsupp.add_closure_Union_range_single

added theorem finsupp.add_hom_ext

modified theorem finsupp.hom_ext

added def finsupp.lift_add_hom

added theorem finsupp.lift_add_hom_apply

added theorem finsupp.lift_add_hom_single_add_hom

added theorem finsupp.lift_add_hom_symm_apply

added theorem finsupp.prod_of_support_subset

modified theorem finsupp.prod_single_index

added def finsupp.single_add_hom