{p q : MvPolynomial (Fin d) ℂ} (hp : RealCoeff p) (hq : RealCoeff q) : RealCoeff (p * q)

Proved

BookProof.YangMillsHermite.RealCoeff.mul

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

qymtimepieceyang-mills

Lean 4 theorem BookProof.YangMillsHermite.RealCoeff.mul (module BookProof.YangMillsHermite), source chapter BookProof/ChapterYangMillsHermite.lean.

Preamble

-- Generated from ChapterYangMillsHermite.lean — theorem BookProof.YangMillsHermite.RealCoeff.mul
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.RealCoeff.mul {p q : MvPolynomial (Fin d) ℂ} (hp : RealCoeff p) (hq : RealCoeff q) :
    RealCoeff (p * q) := by sorry

Source

https://github.com/leonardopedro/timepiece/blob/61595bc/BookProof/ChapterYangMillsHermite.lean

View graph