`BookProof.ChapterCoherentOverlapComplex.norm_ofRealVec` (q : EuclideanSpace ℝ (Fin n)) : ‖ofRealVec q‖ = ‖q‖

Initializing...

`BookProof.ChapterCoherentOverlapComplex.norm_ofRealVec` (q : EuclideanSpace ℝ (Fin n)) : ‖ofRealVec q‖ = ‖q‖ · Prove2Me