`BookProof.ChapterDeterministic.commute_projSet_measOpSet_iff_isDeterministic` (U : Matrix (Fin n) (Fin n) ℂ) : (∀ A B : Finset (Fin n), Commute (projSet A) (measOpSet U B)) ↔ IsDe

Proved

BookProof.ChapterDeterministic.commute_projSet_measOpSet_iff_isDeterministic

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

theoremstimepiece

Prove the following Lean 4 theorem from ChapterDeterministic.

BookProof.ChapterDeterministic.commute_projSet_measOpSet_iff_isDeterministic (U : Matrix (Fin n) (Fin n) ℂ) : (∀ A B : Finset (Fin n), Commute (projSet A) (measOpSet U B)) ↔ IsDeterministic U

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

Preamble

-- Generated from ChapterDeterministic.lean — theorem BookProof.ChapterDeterministic.commute_projSet_measOpSet_iff_isDeterministic
import Mathlib
import Definitions.Def_ChapterDeterministic
import Definitions.Def_ChapterElectroweakFieldStrength
import Definitions.Def_ChapterReconstruct
import Definitions.Def_ChapterTimeTranslation
open BookProof.ChapterElectroweakFieldStrength
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_projSet_measOpSet_iff_isDeterministic
    (U : Matrix (Fin n) (Fin n) ℂ) :
    (∀ A B : Finset (Fin n), Commute (projSet A) (measOpSet U B)) ↔ IsDeterministic U := by sorry

View graph