[math-classes] Should the inner product be proper with respect to equivalence?

[langston-barrett]

In our discussion on #30, we decided that sm should be proper with respect to equiv. Does that same reasoning hold for inprod? My intuition tells me it should, as I need that property to prove the following lemma about orthogonal projections:

Section orthogonal_projection.
  Context `{InnerProductSpace K V}.

  Definition proj (u v : V) : V := (⟨ u , v ⟩ / (⟨ u , u ⟩)) · u.

  Lemma lemma1 : forall (c : K) (u1 u2 v : V), u1 = c · u2 -> proj u1 v = proj u2 v.

Adding the following lines to vectorspace.v allows me to rewrite using the equality hypothesis:

Notation "(⟨⟩)" := (inprod) (only parsing) : mc_scope.
[...]
Class InnerProductSpace (K V : Type)
[...]
   ; inprod_proper  :> Proper ((=) ==> (=) ==> (=)) (⟨⟩)

I'm happy to make a pull request if this seems appropriate!

[spitters]

Yes! Thanks for spotting that. Please send a PR.

[langston-barrett]

Fixed in coq-community/math-classes#17