Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-04-23 05:39 4ad7dc9d

View on Github →

chore(algebra/ring/equiv): protect ring equiv lemmas for big operators (#13624)

Estimated changes

Modified src/algebra/ring/equiv.lean

deleted theorem ring_equiv.map_list_prod

deleted theorem ring_equiv.map_list_sum

deleted theorem ring_equiv.map_multiset_prod

deleted theorem ring_equiv.map_multiset_sum

deleted theorem ring_equiv.map_prod

deleted theorem ring_equiv.map_sum

deleted theorem ring_equiv.unop_map_list_prod