Bennett Homogenization Term

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

section
open Finset

namespace D1Bound5

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






theorem _root_.D1Bound5.bennettHomogenizationTerm (k h : ℕ) (hh : h ≤ k)
    (a N : F) (hN : N ≠ 0) :
    N ^ k * ((N⁻¹) ^ h * (1 + a * N⁻¹) ^ (k - h)) =
      (N + a) ^ (k - h) := by sorry



section Nodes

variable {I : Type*} [DecidableEq I]







end Nodes

end D1Bound5
end