Homogeneous Multiset Sum equiv

import Mathlib.Data.Finset.Insert
import Mathlib.Data.Sym.Basic
import Mathlib.LinearAlgebra.Lagrange
import Mathlib.RingTheory.MvPolynomial.Symmetric.Defs
import Definitions.Def_D1Bound5_HomogeneousSymmetric_Definitions

section
open Polynomial Finset

namespace D1Bound5


theorem _root_.D1Bound5.homogeneousMultisetSum_equiv
    {ι κ R : Type*} [Fintype ι] [DecidableEq ι]
    [Fintype κ] [DecidableEq κ] [CommSemiring R]
    (e : ι ≃ κ) (a : κ → R) (n : ℕ) :
    homogeneousMultisetSum (fun i => a (e i)) n = homogeneousMultisetSum a n := by sorry









end D1Bound5
end