@@ -299,27 +299,31 @@ class (VerifiedRing a, Field a) => VerifiedField a where
299299 total fieldInverseIsInverseL : (l : a) -> l <*> inverseM l = unity
300300 total fieldInverseIsInverseR : (r : a) -> inverseM r <*> r = unity
301301
302−||| A Vector Space over a Field can be considered as an additive Abeliean Group
303−||| of Vectors adjoined to the Field structure with a scale operation multiplying
304−||| vectors by field elements, and distributivity laws relating the scale
305−||| operation to both field addition and vector space addition. Must satisfy the
306−||| following laws:
302+||| A module over a ring is an additive abeliean group of 'vectors' endowed with a
303+||| scale operation multiplying vectors by ring elements, and distributivity laws
304+||| relating the scale operation to both ring addition and module addition.
305+||| Must satisfy the following laws:
307306|||
308−||| + Compatibility of scalar multiplication with field multiplication:
307+||| + Compatibility of scalar multiplication with ring multiplication:
309308||| forall a b v, a <#> (b <#> v) = (a <*> b) <#> v
310−||| + Field unity is the identity element of scalar multiplication:
309+||| + Ring unity is the identity element of scalar multiplication:
311310||| forall v, unity <#> v = v
312311||| + Distributivity of `<#>` and `<+>`:
313312||| forall a v w, a <#> (v <+> w) == (a <#> v) <+> (a <#> w)
314313||| forall a b v, (a <+> b) <#> v == (a <#> v) <+> (b <#> v)
315−class (Field a, AbelianGroup b) => VectorSpace a b where
314+class (RingWithUnity a, AbelianGroup b) => Module a b where
316315 (<#>) : a -> b -> b
317316
318−class (VerifiedField a, VerifiedAbelianGroup b, VectorSpace a b) => VerifiedVectorSpace a b where
319− total vectorspaceScalarMultiplyComposition : (x,y : a) -> (v : b) -> x <#> (y <#> v) = (x <*> y) <#> v
320− total vectorspaceScalarUnityIsUnity : (v : b) -> unity <#> v = v
321− total vectorspaceScalarMultDistributiveWRTVectorAddition : (s : a) -> (v, w : b) -> s <#> (v <+> w) = (s <#> v) <+> (s <#> w)
322− total vectorspaceScalarMultDistributiveWRTFieldAddition : (s, t : a) -> (v : b) -> (s <+> t) <#> v = (s <#> v) <+> (t <#> v)
317+class (VerifiedRingWithUnity a, VerifiedAbelianGroup b, Module a b) => VerifiedModule a b where
318+ total moduleScalarMultiplyComposition : (x,y : a) -> (v : b) -> x <#> (y <#> v) = (x <*> y) <#> v
319+ total moduleScalarUnityIsUnity : (v : b) -> unity <#> v = v
320+ total moduleScalarMultDistributiveWRTVectorAddition : (s : a) -> (v, w : b) -> s <#> (v <+> w) = (s <#> v) <+> (s <#> w)
321+ total moduleScalarMultDistributiveWRTModuleAddition : (s, t : a) -> (v : b) -> (s <+> t) <#> v = (s <#> v) <+> (t <#> v)
322+
323+||| A vector space is a module over a ring that is also a field
324+class (Field a, Module a b) => VectorSpace a b where
325+
326+class (VerifiedField a, VerifiedModule a b) => VerifiedVectorSpace a b where {}
323327
324328-- XXX todo:
325329-- Structures where "abs" make sense.