Bennett coeff mul trunc

import Lean.Elab.Tactic.Omega
import Mathlib.Algebra.Polynomial.BigOperators
import Mathlib.Algebra.Polynomial.Degree.Operations
import Mathlib.Algebra.Polynomial.Div
import Mathlib.Algebra.Polynomial.PartialFractions
import Mathlib.Algebra.Polynomial.RingDivision
import Mathlib.LinearAlgebra.Matrix.Polynomial
import Mathlib.RingTheory.PowerSeries.Binomial
import Mathlib.RingTheory.PowerSeries.Trunc
import Mathlib.Tactic.Ring

section
open Finset

namespace D1Bound5

variable {F : Type*} [Field F] [CharZero F]



section Nodes

variable {I : Type*} [Fintype I] [DecidableEq I]




theorem _root_.D1Bound5.bennett_coeff_mul_trunc (P θ : PowerSeries F) (D r : ℕ) (hr : r < D) :
    PowerSeries.coeff r (P * (PowerSeries.trunc D θ : PowerSeries F)) =
      PowerSeries.coeff r (P * θ) := by sorry







end Nodes

end D1Bound5
end