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

Proved

BookProof.ChapterDeterministic.measOp_mul_proj_apply

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

theoremstimepiece

Prove the following Lean 4 theorem from ChapterDeterministic.

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

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

Preamble

-- Generated from ChapterDeterministic.lean — theorem BookProof.ChapterDeterministic.measOp_mul_proj_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.measOp_mul_proj_apply (U : Matrix (Fin n) (Fin n) ℂ) (a b i j : Fin n) :
    (measOp U b * proj a) i j =
      if j = a then U i b * (starRingEnd ℂ) (U a b) else 0 := by sorry

View graph