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_hom`s. I'm very open to suggestions about where they should go; `map_fpow` in particular requires a new import in `algebra/field_power.lean`.

src/algebra/field_power.lean

@@ -5,6 +5,7 @@ Authors: Robert Y. Lewis
 -/
 import algebra.group_with_zero.power
 import tactic.linarith
+import data.equiv.ring
 
 /-!
 # Integer power operation on fields and division rings
@@ -19,6 +20,10 @@ universe u
   ∀ (a : K) (n : ℤ), f (a ^ n) = f a ^ n :=
 f.to_monoid_with_zero_hom.map_fpow
 
+@[simp] lemma ring_equiv.map_fpow {K L : Type*} [division_ring K] [division_ring L] (f : K ≃+* L) :
+  ∀ (a : K) (n : ℤ), f (a ^ n) = f a ^ n :=
+f.to_ring_hom.map_fpow
+
 @[simp] lemma fpow_bit0_neg {K : Type*} [division_ring K] (x : K) (n : ℤ) :
   (-x) ^ (bit0 n) = x ^ bit0 n :=
 by rw [fpow_bit0', fpow_bit0', neg_mul_neg]

src/data/equiv/ring.lean

@@ -386,6 +386,27 @@ g.to_ring_hom.map_sum f s
 
 end big_operators
 
+section division_ring
+
+variables {K K' : Type*} [division_ring K] [division_ring K']
+  (g : K ≃+* K') (x y : K)
+
+lemma map_inv : g x⁻¹ = (g x)⁻¹ := g.to_ring_hom.map_inv x
+
+lemma map_div : g (x / y) = g x / g y := g.to_ring_hom.map_div x y
+
+end division_ring
+
+section group_power
+
+variables [semiring R] [semiring S]
+
+@[simp] lemma map_pow (f : R ≃+* S) (a) :
+  ∀ n : ℕ, f (a ^ n) = (f a) ^ n :=
+f.to_ring_hom.map_pow a
+
+end group_power
+
 end ring_equiv
 
 namespace mul_equiv