Reciprocal vandermonde reverse

import Mathlib.LinearAlgebra.Lagrange

section
open Polynomial Finset

namespace D1Bound5






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







end D1Bound5
end