`BookProof.ChapterCoherentOverlap.coherentOverlap_eq_one_iff` (q k : EuclideanSpace ℝ (Fin n)) : coherentOverlap q k = 1 ↔ q = k

Initializing...

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