`BookProof.ChapterDeterministic.commute_proj_measOp_iff_isDeterministicCol` (U : Matrix (Fin n) (Fin n) ℂ) (b : Fin n) : (∀ a : Fin n, Commute (proj a) (measOp U b)) ↔ IsDeterminis

Proved

BookProof.ChapterDeterministic.commute_proj_measOp_iff_isDeterministicCol

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

theoremstimepiece

Prove the following Lean 4 theorem from ChapterDeterministic.

BookProof.ChapterDeterministic.commute_proj_measOp_iff_isDeterministicCol (U : Matrix (Fin n) (Fin n) ℂ) (b : Fin n) : (∀ a : Fin n, Commute (proj a) (measOp U b)) ↔ IsDeterministicCol U b

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

Preamble

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


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


variable {n : ℕ}

Formal statement

theorem BookProof.ChapterDeterministic.commute_proj_measOp_iff_isDeterministicCol
    (U : Matrix (Fin n) (Fin n) ℂ) (b : Fin n) :
    (∀ a : Fin n, Commute (proj a) (measOp U b)) ↔ IsDeterministicCol U b := by sorry

View graph