`BookProof.ChapterGaugeAdjointAlgebra.weylEnergy_gauge_invariant` {κ : L → L → ℝ} (hinv : ∀ x y z : L, κ ⁅x, z⁆ y + κ x ⁅y, z⁆ = 0) (hsymm : ∀ x y : L, κ x y = κ y x) (π :...

Proved

BookProof.ChapterGaugeAdjointAlgebra.weylEnergy_gauge_invariant

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

theoremstimepiece

Prove the following Lean 4 theorem from ChapterGaugeAdjointAlgebra.

BookProof.ChapterGaugeAdjointAlgebra.weylEnergy_gauge_invariant {κ : L → L → ℝ} (hinv : ∀ x y z : L, κ ⁅x, z⁆ y + κ x ⁅y, z⁆ = 0) (hsymm : ∀ x y : L, κ x y = κ y x) (π : Fin 3 → L) (B : Fin 3 → Fin 3 → L) (θ : L) : (∑ i, κ ⁅π i, θ⁆ (π i)) + (1 / 2) * ∑ i, ∑ j, κ ⁅B i j, θ⁆ (B i j) = 0

Formalization note: Lean 4 identifier BookProof.ChapterGaugeAdjointAlgebra.weylEnergy_gauge_invariant.

Preamble

-- Generated from ChapterGaugeAdjointAlgebra.lean — theorem BookProof.ChapterGaugeAdjointAlgebra.weylEnergy_gauge_invariant
import Mathlib
import Definitions.Def_ChapterGaugeAdjointAlgebra
open BookProof.ChapterGaugeAdjointAlgebra




open Finset

variable {L : Type*} [LieRing L]

Formal statement

theorem BookProof.ChapterGaugeAdjointAlgebra.weylEnergy_gauge_invariant {κ : L → L → ℝ}
    (hinv : ∀ x y z : L, κ ⁅x, z⁆ y + κ x ⁅y, z⁆ = 0)
    (hsymm : ∀ x y : L, κ x y = κ y x)
    (π : Fin 3 → L) (B : Fin 3 → Fin 3 → L) (θ : L) :
    (∑ i, κ ⁅π i, θ⁆ (π i)) + (1 / 2) * ∑ i, ∑ j, κ ⁅B i j, θ⁆ (B i j) = 0 := by sorry

View graph