Commit 2021-10-08 17:52 91ee8f1d

View on Github →

chore(data/equiv/ring): add big operator lemmas for ring equivs (#9628) This PR adds lemmas involving big operators (such as map_sum, map_prod, etc) for ring_equivs.

Estimated changes

Modified src/data/equiv/ring.lean

added theorem ring_equiv.map_list_prod

added theorem ring_equiv.map_list_sum

added theorem ring_equiv.map_multiset_prod

added theorem ring_equiv.map_multiset_sum

added theorem ring_equiv.map_prod

added theorem ring_equiv.map_sum