`BookProof.ChapterF4.unitary_preserves_dotProduct` {n : ℕ} (U : Matrix (Fin n) (Fin n) ℂ) (hU : Uᴴ * U = 1) (x y : Fin n → ℂ) : star (U.mulVec x) ⬝ᵥ U.mulVec y = star x ⬝ᵥ y

Initializing...

`BookProof.ChapterF4.unitary_preserves_dotProduct` {n : ℕ} (U : Matrix (Fin n) (Fin n) ℂ) (hU : Uᴴ * U = 1) (x y : Fin n → ℂ) : star (U.mulVec x) ⬝ᵥ U.mulVec y = star x ⬝ᵥ y · Prove2Me