Bennett Reciprocal Infinity mul

import Lean.Elab.Tactic.Omega
import Mathlib.Algebra.Polynomial.BigOperators
import Mathlib.Algebra.Polynomial.PartialFractions
import Mathlib.Algebra.Polynomial.Reverse
import Mathlib.Algebra.Polynomial.RingDivision
import Mathlib.RingTheory.PowerSeries.Binomial
import Mathlib.Tactic.Ring
import Definitions.Def_D1Bound5_BennettPartialFractions_Definitions
import Definitions.Def_D1Bound5_BennettResiduesAtInfinity_Definitions

section
open Finset Polynomial

namespace D1Bound5

section Reverse

variable {F : Type*} [Field F]



end Reverse

section Residues

variable {F ι : Type*} [Field F] [CharZero F]
variable [Fintype ι] [DecidableEq ι]














theorem _root_.D1Bound5.bennettReciprocalInfinity_mul
    (a : ι → F) (e : ι → ℕ) :
    ((bennettPoleDenominator a e).reverse : PowerSeries F) *
      bennettReciprocalInfinity a e = 1 := by sorry



end Residues

end D1Bound5
end