fix(*): Lemma rename

leanprover-community · Nov 7, 2020 · 208af0f · 208af0f
1 parent 63315a3
commit 208af0f
Showing 1 changed file with 2 additions and 2 deletions.
diff --git a/src/algebra/polynomial/group_ring_action.lean b/src/algebra/polynomial/group_ring_action.lean
@@ -67,11 +67,11 @@ variables (G : Type*) [group G]
 
 theorem eval_smul' [mul_semiring_action G S] (g : G) (f : polynomial S) (x : S) :
   f.eval (g • x) = g • (g⁻¹ • f).eval x :=
-by rw [← smul_eval_smul, mul_action.smul_inv_smul]
+by rw [← smul_eval_smul, smul_inv_smul]
 
 theorem smul_eval [mul_semiring_action G S] (g : G) (f : polynomial S) (x : S) :
   (g • f).eval x = g • f.eval (g⁻¹ • x) :=
-by rw [← smul_eval_smul, mul_action.smul_inv_smul]
+by rw [← smul_eval_smul, smul_inv_smul]
 
 end polynomial