Bennett Pole Series mul

import Mathlib.RingTheory.PowerSeries.Binomial
import Mathlib.Tactic.Ring
import Definitions.Def_D1Bound5_BennettPoleSeries_Definitions

section
open PowerSeries

namespace D1Bound5

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








theorem _root_.D1Bound5.bennettPoleSeries_mul (d : F) (hd : d ≠ 0) (k : ℕ) :
    (PowerSeries.C d + PowerSeries.X : PowerSeries F) ^ k * bennettPoleSeries d k = 1 := by sorry

end D1Bound5
end