Commit 2020-10-31 08:43 3b2c97f9

View on Github →

feat(data/dfinsupp): Port finsupp.lsum and lemmas about lift_add_hom (#4833) This then removes the proofs of any direct_sum lemmas which become equivalent to the lift_add_hom lemmas

Estimated changes

Modified src/algebra/direct_sum.lean

Modified src/data/dfinsupp.lean

added theorem dfinsupp.comp_lift_add_hom

added theorem dfinsupp.lhom_ext'

added theorem dfinsupp.lhom_ext

added theorem dfinsupp.lift_add_hom_apply_single

added theorem dfinsupp.lift_add_hom_comp_single

added theorem dfinsupp.lift_add_hom_single_add_hom

added def dfinsupp.lsum

added theorem dfinsupp.sum_add_hom_comp_single

Modified src/linear_algebra/direct_sum_module.lean