mathlib3

91ee8f1d - chore(data/equiv/ring): add big operator lemmas for ring equivs (#9628)

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_equiv`s.