refactor(data/polynomial/{coeff,monomial}): move smul_eq_C_mul (#9287)

This moves `smul_eq_C_mul` from `monomial.lean` into `coeff.lean` so that the import on `monomial.lean` can be changed from `data.polynomial.coeff` to `data.polynomial.basic`. This should shave about 10 seconds off the [longest pole for parallelized mathlib compilation](https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/The.20long.20pole.20in.20mathlib/near/253932389).

src/data/polynomial/coeff.lean

@@ -206,6 +206,8 @@ lemma coeff_bit1_mul (P Q : polynomial R) (n : ℕ) :
   coeff (bit1 P * Q) n = 2 * coeff (P * Q) n + coeff Q n :=
 by simp [bit1, add_mul, coeff_bit0_mul]
 
+lemma smul_eq_C_mul (a : R) : a • p = C a * p := by simp [ext_iff]
+
 end coeff
 
 section cast

src/data/polynomial/monomial.lean

@@ -3,7 +3,7 @@ Copyright (c) 2018 Chris Hughes. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Chris Hughes, Johannes Hölzl, Scott Morrison, Jens Wagemaker
 -/
-import data.polynomial.coeff
+import data.polynomial.basic
 
 /-!
 # Univariate monomials
@@ -23,8 +23,6 @@ lemma monomial_one_eq_iff [nontrivial R] {i j : ℕ} :
   (monomial i 1 : polynomial R) = monomial j 1 ↔ i = j :=
 by simp [monomial, monomial_fun, finsupp.single_eq_single_iff]
 
-lemma smul_eq_C_mul (a : R) : a • p = C a * p := by simp [ext_iff]
-
 instance [nontrivial R] : infinite (polynomial R) :=
 infinite.of_injective (λ i, monomial i 1) $
 λ m n h, by simpa [monomial_one_eq_iff] using h