{t : ℝ} {p : MvPolynomial (Fin d) ℂ} (hp : RealCoeff p) : RealCoeff ((t : ℂ) • p)

Proved

BookProof.YangMillsHermite.RealCoeff.smul

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

qymtimepieceyang-mills

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

Preamble

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

Source

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

View graph