Homogeneous Multiset Sum zero

import Mathlib.Data.Sym.Basic
import Mathlib.RingTheory.MvPolynomial.Symmetric.Defs
import Definitions.Def_D1Bound5_HomogeneousSymmetric_Definitions

section
open Finset Multiset Sym

namespace D1Bound5








@[simp] theorem _root_.D1Bound5.homogeneousMultisetSum_zero
    {ι R : Type*} [Fintype ι] [DecidableEq ι] [CommSemiring R]
    (a : ι → R) : homogeneousMultisetSum a 0 = 1 := by sorry







end D1Bound5
end