Add constantCoeff_smul to RingTheory.PowerSeries.Basic (#12616)

```
example : (constantCoeff ℝ) ((2:ℝ)•X) = 0 := by simp
```
simp doesn't solve the above because there is no lemma constantCoeff_smul tagged simp. This PR adds it to RingTheory.PowerSeries.Basic.



Co-authored-by: sgouezel <sebastien.gouezel@univ-rennes1.fr>

Mathlib/RingTheory/PowerSeries/Basic.lean

@@ -355,6 +355,11 @@ theorem coeff_smul {S : Type*} [Semiring S] [Module R S] (n : ℕ) (φ : PowerSe
   rfl
 #align power_series.coeff_smul PowerSeries.coeff_smul
 
+@[simp]
+theorem constantCoeff_smul {S : Type*} [Semiring S] [Module R S] (φ : PowerSeries S) (a : R) :
+    constantCoeff S (a • φ) = a • constantCoeff S φ :=
+  rfl
+
 theorem smul_eq_C_mul (f : R⟦X⟧) (a : R) : a • f = C R a * f := by
   ext
   simp