Prove2Me

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

Proved
BookProof.YangMillsHermite.PolySym.comp_adj

by leonardopedro · Sep 10, 2026 · Mathlib 0df444a (Lean v4.33.1)

qymtimepieceyang-mills

Lean 4 theorem BookProof.YangMillsHermite.PolySym.comp_adj (module BookProof.YangMillsHermite), source chapter BookProof/ChapterYangMillsHermite.lean.

Preamble
-- Generated from ChapterYangMillsHermite.lean — theorem BookProof.YangMillsHermite.PolySym.comp_adj
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 : ℕ}
Formal statement
theorem BookProof.YangMillsHermite.PolySym.comp_adj {S T : Module.End ℂ (MvPolynomial (Fin d) ℂ)}
    (hS : PolySym S) (hT : PolySym T) : PolyAdj (S.comp T) (T.comp S) := by sorry
Source
https://github.com/leonardopedro/timepiece/blob/61595bc/BookProof/ChapterYangMillsHermite.lean

View graph