`BookProof.ChapterA.inner_self_complex_iff_real` (T : H₁ → H₂) : (∀ x, (inner ℂ (T x) (T x) : ℂ) = (inner ℂ x x : ℂ)) ↔ (∀ x, (inner ℝ (T x) (T x) : ℝ) = (inner ℝ x x : ℝ))

Initializing...

`BookProof.ChapterA.inner_self_complex_iff_real` (T : H₁ → H₂) : (∀ x, (inner ℂ (T x) (T x) : ℂ) = (inner ℂ x x : ℂ)) ↔ (∀ x, (inner ℝ (T x) (T x) : ℝ) = (inner ℝ x x : ℝ)) · Prove2Me