`BookProof.ChapterWeakValue.hadamard_psi0` : (H *ᵥ psi0) = ![(1 / Real.sqrt 2 : ℂ), (1 / Real.sqrt 2 : ℂ)]
ProvedBookProof.ChapterWeakValue.hadamard_psi0theoremstimepiece
Prove the following Lean 4 theorem from ChapterWeakValue.
BookProof.ChapterWeakValue.hadamard_psi0 : (H *ᵥ psi0) = ![(1 / Real.sqrt 2 : ℂ), (1 / Real.sqrt 2 : ℂ)]
Formalization note: Lean 4 identifier BookProof.ChapterWeakValue.hadamard_psi0.
Preamble
-- Generated from ChapterWeakValue.lean — theorem BookProof.ChapterWeakValue.hadamard_psi0
import Mathlib
import Definitions.Def_ChapterWeakValue
import Definitions.Def_ChapterDoubleSlit
open BookProof.ChapterDoubleSlit
open BookProof.ChapterWeakValue
open scoped BigOperators Matrix
variable {n : ℕ}Formal statement
theorem BookProof.ChapterWeakValue.hadamard_psi0 : (H *ᵥ psi0) = ![(1 / Real.sqrt 2 : ℂ), (1 / Real.sqrt 2 : ℂ)] := by sorry