`BookProof.ChapterDeterministic.proj_mul_measOp_apply` (U : Matrix (Fin n) (Fin n) ℂ) (a b i j : Fin n) : (proj a * measOp U b) i j = if i = a then U a b * (starRingEnd ℂ) (U j b)

Proved

BookProof.ChapterDeterministic.proj_mul_measOp_apply

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

theoremstimepiece

Prove the following Lean 4 theorem from ChapterDeterministic.

BookProof.ChapterDeterministic.proj_mul_measOp_apply (U : Matrix (Fin n) (Fin n) ℂ) (a b i j : Fin n) : (proj a * measOp U b) i j = if i = a then U a b * (starRingEnd ℂ) (U j b) else 0

Formalization note: Lean 4 identifier BookProof.ChapterDeterministic.proj_mul_measOp_apply.

Preamble

-- Generated from ChapterDeterministic.lean — theorem BookProof.ChapterDeterministic.proj_mul_measOp_apply
import Definitions.Def_ChapterReconstruct
import Mathlib
import Definitions.Def_ChapterDeterministic
import Definitions.Def_ChapterElectroweakFieldStrength
import Definitions.Def_ChapterTimeTranslation
open BookProof.ChapterTimeTranslation
open BookProof.ChapterDeterministic


open scoped BigOperators
open Finset Matrix
open BookProof.ChapterReconstruct BookProof.ChapterTimeTranslation


variable {n : ℕ}

Formal statement

theorem BookProof.ChapterDeterministic.proj_mul_measOp_apply (U : Matrix (Fin n) (Fin n) ℂ) (a b i j : Fin n) :
    (proj a * measOp U b) i j =
      if i = a then U a b * (starRingEnd ℂ) (U j b) else 0 := by sorry

View graph