search

coq-community / math-classes

A library of abstract interfaces for mathematical structures in Coq [maintainer=@spitters,@Lysxia]
https://math-classes.github.io
MIT License
162 stars 43 forks source link

Fix inner product space laws #49

Open langston-barrett opened 6 years ago

langston-barrett commented 6 years ago

One needs the additional axioms, see #15.

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