Reciprocal anchor weight standard

import Mathlib.LinearAlgebra.Lagrange

section
open Polynomial Finset

namespace D1Bound5








theorem _root_.D1Bound5.reciprocal_anchor_weight_standard
    {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)) =
      (-1 : F) ^ (s.card - 1) * (∏ j ∈ s, a j)⁻¹ *
        ((a i)⁻¹) ^ (k + s.card - 1) /
        (∏ j ∈ s.erase i, ((a i)⁻¹ - (a j)⁻¹)) := by sorry





end D1Bound5
end