[STATEMENT]
lemma ZmX_carrier:
  shows "ZmX \<in> carrier_mat 2 2"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ZmX \<in> carrier_mat 2 2
[PROOF STEP]
unfolding ZmX_def X_def Z_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. complex_of_real (1 / sqrt 2) \<cdot>\<^sub>m (Matrix.mat 2 2 (\<lambda>(i, j). if i \<noteq> j then 0 else if i = 0 then 1 else - 1) - Matrix.mat 2 2 (\<lambda>(i, j). if i = j then 0 else 1)) \<in> carrier_mat 2 2
[PROOF STEP]
by (simp add: minus_carrier_mat')