Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2020-04-10 18:03 29080c8c

View on Github →

feat(data/list/range): add sum lemmas (#2385) Adding the proof that left and right multiplication in a ring commute with list sum.

Estimated changes

Modified src/algebra/group/hom.lean

modified theorem add_monoid_hom.map_sub

added def add_monoid_hom.mul_left

added def add_monoid_hom.mul_right

Modified src/data/list/basic.lean

added theorem list.prod_map_hom

added theorem list.sum_map_mul_left

added theorem list.sum_map_mul_right

Modified src/data/list/range.lean

added theorem list.prod_range_succ'