`BookProof.ChapterA.rimaginary_orthogonal` (J : W ≃ₗᵢ[ℝ] W) (hJ : ∀ x, J (J x) = -x) (x : W) : inner ℝ (J x) x = 0

Initializing...

`BookProof.ChapterA.rimaginary_orthogonal` (J : W ≃ₗᵢ[ℝ] W) (hJ : ∀ x, J (J x) = -x) (x : W) : inner ℝ (J x) x = 0 · Prove2Me