Homogeneous Multiset Sum singleton

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_singleton
    {ι R : Type*} [DecidableEq ι] [CommSemiring R]
    (a : ι → R) (t : ι) (n : ℕ) :
    homogeneousMultisetSum (fun i : ({t} : Finset ι) => a i) n = (a t)^n := by sorry





end D1Bound5
end