Reciprocal vandermonde product

import Mathlib.LinearAlgebra.Lagrange

section
open Polynomial Finset

namespace D1Bound5


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











end D1Bound5
end