`BookProof.ChapterA3q.projMixed_mul_projAnti` {N : ℕ} (hN : 2 ≤ N) : projMixed N * projAnti N = 0

Initializing...

`BookProof.ChapterA3q.projMixed_mul_projAnti` {N : ℕ} (hN : 2 ≤ N) : projMixed N * projAnti N = 0 · Prove2Me