feat(PowerSeries): coefficients of series products (#14452)

Add three elementary lemmas about coefficients of series products.

Author: rwst

Mathlib/RingTheory/PowerSeries/Basic.lean

@@ -673,6 +673,36 @@ theorem coeff_prod (f : ι → PowerSeries R) (d : ℕ) (s : Finset ι) :
     Equiv.coe_toEmbedding, Finsupp.mapRange.equiv_apply, AddEquiv.coe_toEquiv_symm,
     Finsupp.mapRange_apply, AddEquiv.finsuppUnique_symm]
 
+/-- The `n`-th coefficient of the `k`-th power of a power series. -/
+lemma coeff_pow (k n : ℕ) (φ : R⟦X⟧) :
+    coeff R n (φ ^ k) = ∑ l ∈ finsuppAntidiag (range k) n, ∏ i ∈ range k, coeff R (l i) φ := by
+  have h₁ (i : ℕ) : Function.const ℕ φ i = φ := rfl
+  have h₂ (i : ℕ) : ∏ j ∈ range i, Function.const ℕ φ j = φ ^ i := by
+    apply prod_range_induction (fun _ => φ) (fun i => φ ^ i) rfl (congrFun rfl) i
+  rw [← h₂, ← h₁ k]
+  apply coeff_prod (f := Function.const ℕ φ) (d := n) (s := range k)
+
+/-- First coefficient of the product of two power series. -/
+lemma coeff_one_mul (φ ψ : R⟦X⟧) : coeff R 1 (φ * ψ) =
+    coeff R 1 φ * constantCoeff R ψ + coeff R 1 ψ * constantCoeff R φ := by
+  have : Finset.antidiagonal 1 = {(0, 1), (1, 0)} := by exact rfl
+  rw [coeff_mul, this, Finset.sum_insert, Finset.sum_singleton, coeff_zero_eq_constantCoeff,
+    mul_comm, add_comm]
+  norm_num
+
+/-- First coefficient of the `n`-th power of a power series with constant coefficient 1. -/
+lemma coeff_one_pow (n : ℕ) (φ : R⟦X⟧) (hC : constantCoeff R φ = 1) :
+    coeff R 1 (φ ^ n) = n * coeff R 1 φ := by
+  induction n with
+  | zero => simp only [pow_zero, coeff_one, one_ne_zero, ↓reduceIte, Nat.cast_zero, zero_mul]
+  | succ n' ih =>
+      have h₁ (m : ℕ) : φ ^ (m + 1) = φ ^ m * φ := by exact rfl
+      have h₂ : Finset.antidiagonal 1 = {(0, 1), (1, 0)} := by exact rfl
+      rw [h₁, coeff_mul, h₂, Finset.sum_insert, Finset.sum_singleton]
+      simp only [coeff_zero_eq_constantCoeff, map_pow, Nat.cast_add, Nat.cast_one,
+        ih, hC, one_pow, one_mul, mul_one, ← one_add_mul, add_comm]
+      decide
+
 end CommSemiring
 
 section CommRing