Mathlib v3 is deprecated. Go to Mathlib v4

Theorem ring_equiv.map_sum

Modification history

2022-04-23 05:39
src/algebra/ring/equiv.lean
chore(algebra/ring/equiv): protect ring equiv lemmas for big operators (#13624)
Deleted ring_equiv.map_sumView on Github →
2021-10-08 17:52
src/data/equiv/ring.lean
chore(data/equiv/ring): add big operator lemmas for ring equivs (#9628) …
Added ring_equiv.map_sumView on Github →