Commit 2021-10-11 02:26 e32154d1

feat(data/equiv/ring): add basic API lemmas for ring_equiv (#9639) This PR adds the lemmas map_inv, map_div, map_pow and map_fpow for ring_equiv. These lemmas were already available for ring_homs. I'm very open to suggestions about where they should go; map_fpow in particular requires a new import in algebra/field_power.lean.