Bennett Cleared Residue diagonal at node

import Lean.Elab.Tactic.Omega
import Mathlib.Algebra.Polynomial.BigOperators
import Mathlib.Algebra.Polynomial.Degree.Operations
import Mathlib.RingTheory.PowerSeries.Binomial
import Mathlib.Tactic.Ring
import Definitions.Def_D1Bound5_BennettClearedResidues_Definitions

section
open Finset

namespace D1Bound5

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









section Nodes

variable {I : Type*} [DecidableEq I]
















theorem _root_.D1Bound5.bennettClearedResidue_diagonal_at_node
    (s : Finset I) (a : I → F) (k : ℕ) (ν : F) (i : I) :
    (bennettClearedResidue s a k ν i i).eval (-a i) =
      Ring.choose ((k : F) + ν) k *
        ∏ l ∈ s.erase i, ((a i - a l)⁻¹) ^ k := by sorry

end Nodes

end D1Bound5
end