Commit 2020-10-15 16:29 07ee11e7

View on Github →

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

Estimated changes

Modified src/algebra/algebra/basic.lean

added theorem alg_equiv.map_div

added theorem alg_equiv.map_finsupp_prod

added theorem alg_equiv.map_finsupp_sum

added theorem alg_equiv.map_inv

modified theorem alg_equiv.map_neg

added theorem alg_equiv.map_prod

modified theorem alg_equiv.map_sub

added theorem alg_hom.map_finsupp_prod

added theorem alg_hom.map_finsupp_sum