Switch Bra/Ket to use EuclideanSpace

[Timeroot]

Currently Bra and Ket are defined as

structure Ket where
  vec : d → ℂ
  normalized' : ∑ x, ‖vec x‖ ^ 2 = 1

as per the note here, it would be much better to instead define them as

structure Ket where
  vec : EuclideanSpace ℂ d
  normalized' : ‖vec‖ = 1

Although this will break several proofs that need fixing. Accordingly, some of the later definitions should probably change a bit, like

def Ket.normalize (v : d → ℂ) (h : ∃ x, v x ≠ 0) : Ket d :=
  { vec := fun x ↦ v x / √(∑ x : d, ‖v x‖ ^ 2),

should probably become

def Ket.normalize (v : d → ℂ) (h : v ≠ 0) : Ket d :=
  { vec := ‖v‖⁻¹ • v,