feat(RingTheory/PowerSeries/Basic): Polynomial.coe_sub and `Polynom…

…ial.coe_neg` (#19339)

These are analogous to the existing `Polynomial.coe_add` and `Polynomial.coe_zero`, about the coercion from `Polynomial` to `PowerSeries`.

[Zulip thread](https://leanprover.zulipchat.com/#narrow/channel/217875-Is-there-code-for-X.3F/topic/.60.281.20-.20X.20.3A.20.E2.84.A4.5BX.5D.29.2EtoPowerSeries.20.3D.201.20-.20.28PowerSeries.2EX.20.3A.20.E2.84.A4.E2.9F.A6X.E2.9F.A7.29.60/near/483708229).

Mathlib/RingTheory/LaurentSeries.lean

@@ -933,7 +933,7 @@ theorem exists_ratFunc_val_lt (f : K⸨X⸩) (γ : ℤₘ₀ˣ) :
     · erw [hs, ← F_mul, PowerSeries.coe_pow, PowerSeries.coe_X, RatFunc.coe_mul, zpow_neg,
         zpow_ofNat, inv_eq_one_div (RatFunc.X ^ s), RatFunc.coe_div, RatFunc.coe_pow, RatFunc.coe_X,
         RatFunc.coe_one, ← inv_eq_one_div, ← mul_sub, map_mul, map_inv₀, ← PowerSeries.coe_X,
-        valuation_X_pow, ← hs, ← RatFunc.coe_coe, ← coe_sub, ← coe_algebraMap,
+        valuation_X_pow, ← hs, ← RatFunc.coe_coe, ← PowerSeries.coe_sub, ← coe_algebraMap,
         valuation_of_algebraMap, ← Units.val_mk0
         (a := ((Multiplicative.ofAdd f.order : Multiplicative ℤ) : ℤₘ₀)), ← hη]
       apply inv_mul_lt_of_lt_mul₀
@@ -943,8 +943,8 @@ theorem exists_ratFunc_val_lt (f : K⸨X⸩) (γ : ℤₘ₀ˣ) :
   · obtain ⟨s, hs⟩ := Int.exists_eq_neg_ofNat (Int.neg_nonpos_of_nonneg (not_lt.mp ord_nonpos))
     obtain ⟨P, hP⟩ := exists_Polynomial_intValuation_lt (PowerSeries.X ^ s * F) γ
     use P
-    erw [← X_order_mul_powerSeriesPart (neg_inj.1 hs).symm, ← RatFunc.coe_coe, ← coe_sub,
-      ← coe_algebraMap, valuation_of_algebraMap]
+    erw [← X_order_mul_powerSeriesPart (neg_inj.1 hs).symm, ← RatFunc.coe_coe,
+      ← PowerSeries.coe_sub, ← coe_algebraMap, valuation_of_algebraMap]
     exact hP
 
 theorem coe_range_dense : DenseRange ((↑) : RatFunc K → K⸨X⸩) := by
@@ -981,7 +981,7 @@ theorem inducing_coe : IsUniformInducing ((↑) : RatFunc K → K⸨X⸩) := by
     refine ⟨⟨d, by rfl⟩, subset_trans (fun _ _ ↦ pre_R ?_) pre_T⟩
     apply hd
     simp only [sub_zero, Set.mem_setOf_eq]
-    erw [← coe_sub, ← valuation_eq_LaurentSeries_valuation]
+    erw [← RatFunc.coe_sub, ← valuation_eq_LaurentSeries_valuation]
     assumption
   · rintro ⟨_, ⟨hT, pre_T⟩⟩
     obtain ⟨d, hd⟩ := Valued.mem_nhds.mp hT
@@ -993,7 +993,7 @@ theorem inducing_coe : IsUniformInducing ((↑) : RatFunc K → K⸨X⸩) := by
     · refine subset_trans (fun _ _ ↦ ?_) pre_T
       apply hd
       erw [Set.mem_setOf_eq, sub_zero, valuation_eq_LaurentSeries_valuation,
-        coe_sub]
+        RatFunc.coe_sub]
       assumption
 
 theorem continuous_coe : Continuous ((↑) : RatFunc K → K⸨X⸩) :=

Mathlib/RingTheory/PowerSeries/Basic.lean

@@ -758,6 +758,7 @@ namespace Polynomial
 
 open Finsupp Polynomial
 
+section CommSemiring
 variable {R : Type*} [CommSemiring R] (φ ψ : R[X])
 
 -- Porting note: added so we can add the `@[coe]` attribute
@@ -877,6 +878,21 @@ theorem coeToPowerSeries.algHom_apply :
     coeToPowerSeries.algHom A φ = PowerSeries.map (algebraMap R A) ↑φ :=
   rfl
 
+end CommSemiring
+
+section CommRing
+variable {R : Type*} [CommRing R]
+
+@[simp, norm_cast]
+lemma coe_neg (p : R[X]) : ((- p : R[X]) : PowerSeries R) = - p :=
+  coeToPowerSeries.ringHom.map_neg p
+
+@[simp, norm_cast]
+lemma coe_sub (p q : R[X]) : ((p - q : R[X]) : PowerSeries R) = p - q :=
+  coeToPowerSeries.ringHom.map_sub p q
+
+end CommRing
+
 end Polynomial
 
 namespace PowerSeries