`BookProof.ChapterCoherentOverlap.coherentOverlap_self` (q : EuclideanSpace ℝ (Fin n)) : coherentOverlap q q = 1

Initializing...

`BookProof.ChapterCoherentOverlap.coherentOverlap_self` (q : EuclideanSpace ℝ (Fin n)) : coherentOverlap q q = 1 · Prove2Me