[math-classes] Additional axiom on inner product spaces: 0 = ⟨v,v⟩ iff v = mon_unit

[langston-barrett]

The Wikipedia definition of an inner product space has the following extra axiom:

0 = ⟨v,v⟩ <-> v = mon_unit 

which isn't present in the current formalism. Should we rewrite the positivity rules as follows?

   ; in_pos_def1    :> ∀ v, PropHolds (0 ≤ ⟨v,v⟩)
   ; in_pos_def2    :> ∀ v, 0 = ⟨v,v⟩ <-> v = mon_unit
   }.

[spitters]

Yes, well spotted. Also, it would be natural to make a normed space out of an inner product space.

[langston-barrett]

Fixed in coq-community/math-classes#17