[STATEMENT]
lemma norm_pre:
  "inner_prod ket_pre ket_pre = 1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. inner_prod ket_pre ket_pre = 1
[PROOF STEP]
unfolding ket_pre_def scalar_prod_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Sum>i = 0..<dim_vec (conjugate (Matrix.vec N (\<lambda>k. if k = 0 then 1 else 0))). Matrix.vec N (\<lambda>k. if k = 0 then 1 else 0) $ i * conjugate (Matrix.vec N (\<lambda>k. if k = 0 then 1 else 0)) $ i) = 1
[PROOF STEP]
using sum_only_one_neq_0[of "{0..<N}" 0 "\<lambda>i. (if i = 0 then 1 else 0) * cnj (if i = 0 then 1 else 0)"]
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>finite {0..<N}; 0 \<in> {0..<N}; \<And>i. \<lbrakk>i \<in> {0..<N}; i \<noteq> 0\<rbrakk> \<Longrightarrow> (if i = 0 then 1 else 0) * cnj (if i = 0 then 1 else 0) = 0\<rbrakk> \<Longrightarrow> (\<Sum>i = 0..<N. (if i = 0 then 1 else 0) * cnj (if i = 0 then 1 else 0)) = (if 0 = 0 then 1 else 0) * cnj (if 0 = 0 then 1 else 0)

goal (1 subgoal):
 1. (\<Sum>i = 0..<dim_vec (conjugate (Matrix.vec N (\<lambda>k. if k = 0 then 1 else 0))). Matrix.vec N (\<lambda>k. if k = 0 then 1 else 0) $ i * conjugate (Matrix.vec N (\<lambda>k. if k = 0 then 1 else 0)) $ i) = 1
[PROOF STEP]
by auto