`BookProof.ChapterWignerSymmetry.sum_triple` {o i j : ι} (hio : i ≠ o) (hjo : j ≠ o) (hij : i ≠ j) {f : ι → ℂ} (hf : ∀ k, k ≠ o → k ≠ i → k ≠ j → f k = 0) (g : ι →...
ProvedBookProof.ChapterWignerSymmetry.sum_tripletheoremstimepiece
Prove the following Lean 4 theorem from ChapterWignerSymmetry.
BookProof.ChapterWignerSymmetry.sum_triple {o i j : ι} (hio : i ≠ o) (hjo : j ≠ o) (hij : i ≠ j) {f : ι → ℂ} (hf : ∀ k, k ≠ o → k ≠ i → k ≠ j → f k = 0) (g : ι → ℂ) : ∑ k, g k * f k = g o * f o + g i * f i + g j * f j
Formalization note: Lean 4 identifier BookProof.ChapterWignerSymmetry.sum_triple.
Preamble
-- Generated from ChapterWignerSymmetry.lean — theorem BookProof.ChapterWignerSymmetry.sum_triple
import Mathlib
import Definitions.Def_ChapterWignerSymmetry
open BookProof.ChapterWignerSymmetry
open scoped InnerProductSpace ComplexConjugate
open Finset
variable {E : Type*} [NormedAddCommGroup E] [InnerProductSpace ℂ E]
variable {T : E → E}
variable {ι : Type*} [Fintype ι] [DecidableEq ι]Formal statement
theorem BookProof.ChapterWignerSymmetry.sum_triple {o i j : ι} (hio : i ≠ o) (hjo : j ≠ o) (hij : i ≠ j) {f : ι → ℂ}
(hf : ∀ k, k ≠ o → k ≠ i → k ≠ j → f k = 0) (g : ι → ℂ) :
∑ k, g k * f k = g o * f o + g i * f i + g j * f j := by sorry