`BookProof.ChapterGaugeMechanicsCharge.ghost_car` : ChapterG.ghostAnnih (A := Module.End ℂ P) * ChapterG.ghostCreat + ChapterG.ghostCreat * ChapterG.ghostAnnih = 1

Proved

BookProof.ChapterGaugeMechanicsCharge.ghost_car

by leonardopedro · Oct 8, 2026 · Mathlib 0df444a (Lean v4.33.1)

theoremstimepiece

Prove the following Lean 4 theorem from ChapterGaugeMechanicsCharge.

BookProof.ChapterGaugeMechanicsCharge.ghost_car : ChapterG.ghostAnnih (A := Module.End ℂ P) * ChapterG.ghostCreat + ChapterG.ghostCreat * ChapterG.ghostAnnih = 1

Formalization note: Lean 4 identifier BookProof.ChapterGaugeMechanicsCharge.ghost_car.

Preamble

-- Generated from ChapterGaugeMechanicsCharge.lean — theorem BookProof.ChapterGaugeMechanicsCharge.ghost_car
import Mathlib
import Definitions.Def_ChapterGaugeMechanicsCharge
import Definitions.Def_ChapterNavierStokes
open BookProof.NavierStokes
open BookProof.ChapterGaugeMechanicsCharge




open MvPolynomial

Formal statement

theorem BookProof.ChapterGaugeMechanicsCharge.ghost_car :
    ChapterG.ghostAnnih (A := Module.End ℂ P) * ChapterG.ghostCreat
      + ChapterG.ghostCreat * ChapterG.ghostAnnih = 1 := by sorry

View graph