`BookProof.ChapterCoherentDynamics.inner_phaseRotate` (theta : ℝ) (q k : EuclideanSpace ℂ (Fin n)) : (inner ℂ (phaseRotate theta q) (phaseRotate theta k) : ℂ) = inner ℂ q k

Initializing...

`BookProof.ChapterCoherentDynamics.inner_phaseRotate` (theta : ℝ) (q k : EuclideanSpace ℂ (Fin n)) : (inner ℂ (phaseRotate theta q) (phaseRotate theta k) : ℂ) = inner ℂ q k · Prove2Me