`BookProof.ChapterA.conjugation_smul_I_of_neg` (θ : AntiUnitary V) {y : V} (hy : θ y = -y) : θ (Complex.I • y) = Complex.I • y

Initializing...

`BookProof.ChapterA.conjugation_smul_I_of_neg` (θ : AntiUnitary V) {y : V} (hy : θ y = -y) : θ (Complex.I • y) = Complex.I • y · Prove2Me