`BookProof.ChapterE3.eulerJ_sq` (l w : Fin n → ℝ) (hll : ∑ i, l i * l i = 1) (hww : ∑ i, w i * w i = 1) (hlw : ∑ i, l i * w i = 0) : eulerJ l w * eulerJ l w = - (Matrix.vecMulVec l

Proved

BookProof.ChapterE3.eulerJ_sq

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

theoremstimepiece

Prove the following Lean 4 theorem from ChapterE3.

BookProof.ChapterE3.eulerJ_sq (l w : Fin n → ℝ) (hll : ∑ i, l i * l i = 1) (hww : ∑ i, w i * w i = 1) (hlw : ∑ i, l i * w i = 0) : eulerJ l w * eulerJ l w = - (Matrix.vecMulVec l l + Matrix.vecMulVec w w)

Formalization note: Lean 4 identifier BookProof.ChapterE3.eulerJ_sq.

Preamble

-- Generated from ChapterE3.lean — theorem BookProof.ChapterE3.eulerJ_sq
import Mathlib
import Definitions.Def_ChapterE3
open BookProof.ChapterE3


open scoped Matrix BigOperators


variable {n : ℕ}

Formal statement

theorem BookProof.ChapterE3.eulerJ_sq (l w : Fin n → ℝ)
    (hll : ∑ i, l i * l i = 1) (hww : ∑ i, w i * w i = 1)
    (hlw : ∑ i, l i * w i = 0) :
    eulerJ l w * eulerJ l w = - (Matrix.vecMulVec l l + Matrix.vecMulVec w w) := by sorry

View graph