theorem orthogonal_span_toDual_symm {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] (π : E →L[ℝ] ℝ) : spanOrthogonal ((InnerProductSpace.toDual ℝ E).symm π) = LinearMap.ker π