feat(algebra/star): star_gpow and star_fpow (#9661)

One unrelated proof changes as the import additions pulls in a simp lemma that was previously missing, making the call to `ring` no longer necessary.

src/algebra/star/basic.lean

@@ -7,6 +7,8 @@ import tactic.apply_fun
 import algebra.order.ring
 import algebra.opposites
 import algebra.big_operators.basic
+import algebra.group_power.lemmas
+import algebra.field_power
 import data.equiv.ring_aut
 import data.equiv.mul_add_aut
 
@@ -116,6 +118,10 @@ op_injective $
 op_injective $
   ((star_mul_equiv : R ≃* Rᵒᵖ).to_monoid_hom.map_inv x).trans (op_inv (star x)).symm
 
+@[simp] lemma star_gpow [group R] [star_monoid R] (x : R) (z : ℤ) : star (x ^ z) = star x ^ z :=
+op_injective $
+  ((star_mul_equiv : R ≃* Rᵒᵖ).to_monoid_hom.map_gpow x z).trans (op_gpow (star x) z).symm
+
 /-- When multiplication is commutative, `star` preserves division. -/
 @[simp] lemma star_div [comm_group R] [star_monoid R] (x y : R) : star (x / y) = star x / star y :=
 (star_mul_aut : R ≃* R).to_monoid_hom.map_div _ _
@@ -237,6 +243,11 @@ def star_ring_aut [comm_semiring R] [star_ring R] : ring_aut R :=
 op_injective $
   ((star_ring_equiv : R ≃+* Rᵒᵖ).to_ring_hom.map_inv x).trans (op_inv (star x)).symm
 
+@[simp] lemma star_fpow [division_ring R] [star_ring R] (x : R) (z : ℤ) :
+  star (x ^ z) = star x ^ z :=
+op_injective $
+  ((star_ring_equiv : R ≃+* Rᵒᵖ).to_ring_hom.map_fpow x z).trans (op_gpow (star x) z).symm
+
 /-- When multiplication is commutative, `star` preserves division. -/
 @[simp] lemma star_div' [field R] [star_ring R] (x y : R) : star (x / y) = star x / star y :=
 (star_ring_aut : R ≃+* R).to_ring_hom.map_div _ _

src/ring_theory/polynomial/bernstein.lean

@@ -433,7 +433,9 @@ begin
   { congr' 1, simp only [←nat_cast_mul] with push_cast,
     cases k; { simp, ring, }, },
   { simp only [←nat_cast_mul] with push_cast,
-    cases n; { simp, ring, }, },
+    cases n,
+    { simp, },
+    { simp, ring, }, },
 end
 
 end bernstein_polynomial