`BookProof.ChapterGaugeAdjointAlgebra.inner_adjVar_self_eq_zero` {κ : L → L → ℝ} (hinv : ∀ x y z : L, κ ⁅x, z⁆ y + κ x ⁅y, z⁆ = 0) (hsymm : ∀ x y : L, κ x y = κ y x) (x θ...
ProvedBookProof.ChapterGaugeAdjointAlgebra.inner_adjVar_self_eq_zerotheoremstimepiece
Prove the following Lean 4 theorem from ChapterGaugeAdjointAlgebra.
BookProof.ChapterGaugeAdjointAlgebra.inner_adjVar_self_eq_zero {κ : L → L → ℝ} (hinv : ∀ x y z : L, κ ⁅x, z⁆ y + κ x ⁅y, z⁆ = 0) (hsymm : ∀ x y : L, κ x y = κ y x) (x θ : L) : κ ⁅x, θ⁆ x = 0
Formalization note: Lean 4 identifier BookProof.ChapterGaugeAdjointAlgebra.inner_adjVar_self_eq_zero.
Preamble
-- Generated from ChapterGaugeAdjointAlgebra.lean — theorem BookProof.ChapterGaugeAdjointAlgebra.inner_adjVar_self_eq_zero
import Mathlib
import Definitions.Def_ChapterGaugeAdjointAlgebra
open BookProof.ChapterGaugeAdjointAlgebra
open Finset
variable {L : Type*} [LieRing L]Formal statement
theorem BookProof.ChapterGaugeAdjointAlgebra.inner_adjVar_self_eq_zero {κ : L → L → ℝ}
(hinv : ∀ x y z : L, κ ⁅x, z⁆ y + κ x ⁅y, z⁆ = 0)
(hsymm : ∀ x y : L, κ x y = κ y x) (x θ : L) : κ ⁅x, θ⁆ x = 0 := by sorry