feat(Algebra/MvPolynomial/Basic): coeff_C_of_ne_zero and coeff_add_single_C (#39623)

These lemmas are multivariate analogs to `Polynomial.coeff_C_of_ne_zero`, `Polynomial.coeff_C_succ` and `PowerSeries.coeff_C_of_ne_zero` and `PowerSeries.coeff_succ_C`. They are useful for defining partial derivatives for multivariate power series, see PR #39626.

- [x] depends on: #39632

Author: justus-springer

Mathlib/Algebra/MvPolynomial/Basic.lean

@@ -593,6 +593,15 @@ theorem coeff_C [DecidableEq σ] (m) (a) :
     coeff m (C a : MvPolynomial σ R) = if 0 = m then a else 0 :=
   Finsupp.single_apply
 
+theorem coeff_C_of_ne_zero {m : σ →₀ ℕ} (h : m ≠ 0) (a : R) : coeff m (C a) = 0 := by
+  classical rw [coeff_C, if_neg h.symm]
+
+-- The intended use case of this theorem is for `n = 1` (often useful for `pderiv`).
+@[simp]
+theorem coeff_add_single_C {n : ℕ} [NeZero n] {m : σ →₀ ℕ} (a : R) (i : σ) :
+    coeff (m + Finsupp.single i n) (C a) = 0 :=
+  coeff_C_of_ne_zero (fun H ↦ by simpa [NeZero.ne] using congr($(H) i)) a
+
 lemma eq_C_of_isEmpty [IsEmpty σ] (p : MvPolynomial σ R) :
     p = C (p.coeff 0) := by
   obtain ⟨x, rfl⟩ := C_surjective σ p

Mathlib/RingTheory/MvPowerSeries/Basic.lean

@@ -351,6 +351,15 @@ theorem coeff_C [DecidableEq σ] (n : σ →₀ ℕ) (a : R) :
 theorem coeff_zero_C (a : R) : coeff (0 : σ →₀ ℕ) (C a) = a :=
   coeff_monomial_same 0 a
 
+theorem coeff_C_of_ne_zero {n : σ →₀ ℕ} (h : n ≠ 0) (a : R) : coeff n (C a) = 0 := by
+  classical rw [coeff_C, if_neg h]
+
+-- The intended use case of this theorem is for `m = 1` (often useful for `pderiv`).
+@[simp]
+theorem coeff_add_single_C {m : ℕ} [NeZero m] {n : σ →₀ ℕ} (a : R) (i : σ) :
+    coeff (n + single i m) (C a) = 0 :=
+  coeff_C_of_ne_zero (fun H ↦ by simpa [NeZero.ne] using congr($(H) i)) a
+
 @[grind inj]
 theorem C_injective : Function.Injective (C : R → MvPowerSeries σ R) := by
   intro a b h