{S T : Module.End ℂ (MvPolynomial (Fin d) ℂ)} (h : PolyAdj S T) (h' : PolyAdj T S) : PolySym (S + T)

-- Generated from ChapterYangMillsHermite.lean — theorem BookProof.YangMillsHermite.PolyAdj.symm_of
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.PolyAdj.symm_of {S T : Module.End ℂ (MvPolynomial (Fin d) ℂ)}
    (h : PolyAdj S T) (h' : PolyAdj T S) : PolySym (S + T) := by sorry