@@ -298,8 +298,27 @@ class (VerifiedRing a, Field a) => VerifiedField a where
298298 total fieldInverseIsInverseL : (l : a) -> l <*> inverseM l = unity
299299 total fieldInverseIsInverseR : (r : a) -> inverseM r <*> r = unity
300300
301−-- XXX todo:
302301-- vector spaces.
302+||| A Vector Space over a Field can be considered as an additive Abeliean Group
303+||| of Vectors adjoined to the Field structure by distributivity laws relating
304+||| the two operations. Such that we satisfy the following laws:
305+|||
306+||| + Unity for `<*>`:
307+||| forall a, a <*> unity == a
308+||| forall a, unity <*> a == a
309+||| + Distributivity of `<*>` and `<+>`:
310+||| forall a x y, a <*> (x <+> y) == (a <*> x) <+> (a <*> y)
311+||| forall a b x, (a <+> b) <*> x == (a <*> x) <+> (b <*> x)
312+class (Field a, AbelianGroup a) => VectorSpace a a where {}
313+
314+class (VerifiedField a, VerifiedAbelianGroup a, VectorSpace a a) => VerifiedVectorSpace a a where
315+ total vectorspaceScalarUnityIsUnityL : (l : a) -> l <*> unity = l
316+ total vectorspaceScalarUnityIsUnityR : (r : a) -> unity <*> r = r
317+ total vectorspaceScalarIsDistributiveWRTVectorAddition : (s : a) -> (x, y : a) -> s <*> (x <+> y) = (s <*> x) <+> (s <*> y)
318+ total vectorspaceScalarIsDistributiveWRTFieldAddition : (s, t : a) -> (x : a) -> (s <+> t) <*> x = (s <*> x) <+> (t <*> x)
319+
320+
321+-- XXX todo:
303322-- Structures where "abs" make sense.
304323-- Euclidean domains, etc.
305324-- Where to put fromInteger and fromRational?