`BookProof.ChapterCoherentOverlapComplex.norm_coherentOverlapC_le_one` (q k : EuclideanSpace ℂ (Fin n)) : ‖coherentOverlapC q k‖ ≤ 1

Initializing...

`BookProof.ChapterCoherentOverlapComplex.norm_coherentOverlapC_le_one` (q k : EuclideanSpace ℂ (Fin n)) : ‖coherentOverlapC q k‖ ≤ 1 · Prove2Me