feat: port Data.Polynomial.Derivative (#2725)

Co-authored-by: Johan Commelin <johan@commelin.net>
leanprover-community · Mar 9, 2023 · 1e41088 · 1e41088
1 parent 43fb515
commit 1e41088
Show file tree

Hide file tree

Showing 3 changed files with 694 additions and 1 deletion.
diff --git a/Mathlib.lean b/Mathlib.lean
@@ -726,6 +726,7 @@ import Mathlib.Data.Polynomial.Coeff
 import Mathlib.Data.Polynomial.Degree.Definitions
 import Mathlib.Data.Polynomial.Degree.Lemmas
 import Mathlib.Data.Polynomial.Degree.TrailingDegree
+import Mathlib.Data.Polynomial.Derivative
 import Mathlib.Data.Polynomial.EraseLead
 import Mathlib.Data.Polynomial.Eval
 import Mathlib.Data.Polynomial.Induction

diff --git a/Mathlib/Algebra/Ring/Basic.lean b/Mathlib/Algebra/Ring/Basic.lean
@@ -69,7 +69,7 @@ def mulLeft [NonUnitalNonAssocSemiring R] (r : R) :
 
 @[simp]
 theorem coe_mul_left [NonUnitalNonAssocSemiring R] (r : R) :
-    (mulLeft r) = (r * ·) :=
+    (mulLeft r : R → R) = HMul.hMul r :=
   rfl
 #align add_monoid_hom.coe_mul_left AddMonoidHom.coe_mul_left