Commutation of the sampling and hiding measurements

theorem MIPRE.Introspection.synOf_eq_zero_of_not_mem_range {F : Type u_1} [Field F] [Fintype F] [DecidableEq F] [Algebra (ZMod 2) F] {n : ℕ} (w : (Fin n → F) → Matrix (Fin n → F) (Fin n → F) ℂ) (L : (Fin n → F) →ₗ[F] Fin n → F) (a : Fin n → F) (ha : a ∉ L.range) : Weyl.synOf w (⇑L) a = 0

theorem MIPRE.Introspection.commute_matrix_smul {ι : Type u_2} [Fintype ι] {A B : Matrix ι ι ℂ} (h : Commute A B) (c d : ℂ) : Commute (c • A) (d • B)

theorem MIPRE.Introspection.linear_measurements_commute {F : Type u_1} [Field F] [Fintype F] [DecidableEq F] [Algebra (ZMod 2) F] {n : ℕ} (L R : (Fin n → F) →ₗ[F] Fin n → F) (hLR : CL.perp R.ker ≤ L.ker) (a b : Fin n → F) : Commute (Weyl.synOf Weyl.wZ (⇑L) a) (Weyl.synOf Weyl.wX (⇑R) b)

The perpendicular-kernel inclusion makes every sampling projector commute with every hiding projector, including zero projectors at outcomes outside the ranges.