`BookProof.ChapterF4.sign_pair_expectation` (c c' : Fin d) : (∑ ω : Fin d → Bool, sgn (ω c) * sgn (ω c')) = if c = c' then (2 ^ d : ℝ) else 0

Initializing...

`BookProof.ChapterF4.sign_pair_expectation` (c c' : Fin d) : (∑ ω : Fin d → Bool, sgn (ω c) * sgn (ω c')) = if c = c' then (2 ^ d : ℝ) else 0 · Prove2Me