Reciprocal anchor weight term

import Mathlib.LinearAlgebra.Lagrange

section
open Polynomial Finset

namespace D1Bound5




theorem _root_.D1Bound5.reciprocal_anchor_weight_term
    {F ι : Type*} [Field F] [DecidableEq ι]
    (s : Finset ι) (a : ι → F)
    (ha : ∀ j ∈ s, a j ≠ 0) (i : ι) (hi : i ∈ s) (k : ℕ) :
    ((a i)⁻¹) ^ (k + 1) /
      (∏ j ∈ s.erase i, (a i - a j)) =
      (∏ j ∈ s, a j)⁻¹ *
        ((a i)⁻¹) ^ (k + (s.erase i).card) /
        (∏ j ∈ s.erase i, ((a j)⁻¹ - (a i)⁻¹)) := by sorry









end D1Bound5
end