{S T : Module.End ℂ (MvPolynomial (Fin d) ℂ)} (hS : PolySym S) (hT : PolySym T) : PolySym (S + T)

-- Generated from ChapterYangMillsHermite.lean — theorem BookProof.YangMillsHermite.PolySym.add
import Mathlib
import Definitions.Def_ChapterYangMillsHermite
open BookProof.YangMillsHermite







open MeasureTheory Complex MvPolynomial
open BookProof.HermiteProductCore BookProof.FarisLavine BookProof.YangMillsFriedrichs
open BookProof.HermiteGalerkin BookProof.FriedrichsExtension BookProof.HashimotoShiftInvert

noncomputable section

variable {d : ℕ}

theorem BookProof.YangMillsHermite.PolySym.add {S T : Module.End ℂ (MvPolynomial (Fin d) ℂ)}
    (hS : PolySym S) (hT : PolySym T) : PolySym (S + T) := by sorry