basic): Add `map_finsupp_(sum|prod)` to `alg_(hom|equiv)` (#4603)

Commit

5 years ago

feat(algebra/algebra/basic): Add `map_finsupp_(sum|prod)` to `alg_(hom|equiv)` (#4603) Also copies some lemmas from `alg_hom` to `alg_equiv` that were missing

References

#4925 - Make prime-avoidance branch build

Author

eric-wieser

Parents

bb1f5492

mathlib 07ee11e7 - feat(algebra/algebra/basic): Add `map_finsupp_(sum|prod)` to `alg_(hom|equiv)` (#4603)

mathlib
07ee11e7 - feat(algebra/algebra/basic): Add `map_finsupp_(sum|prod)` to `alg_(hom|equiv)` (#4603)