@@ -6,6 +6,7 @@ import Builtins
6infixl 6 <->
6infixl 6 <->
7infixl 6 <+>
7infixl 6 <+>
8infixl 6 <*>
8infixl 6 <*>
10%access public
11%access public
@@ -298,25 +299,27 @@ class (VerifiedRing a, Field a) => VerifiedField a where
298 total fieldInverseIsInverseL : (l : a) -> l <*> inverseM l = unity
299 total fieldInverseIsInverseL : (l : a) -> l <*> inverseM l = unity
299 total fieldInverseIsInverseR : (r : a) -> inverseM r <*> r = unity
300 total fieldInverseIsInverseR : (r : a) -> inverseM r <*> r = unity
302||| A Vector Space over a Field can be considered as an additive Abeliean Group
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
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
304−||| the two operations. Such that we satisfy the following laws:
306+||| following laws:
306−||| + Unity for `<*>`:
308+||| + Compatibility of scalar multiplication with field multiplication:
307−||| forall a, a <*> unity == a
309+||| forall a b v, a <#> (b <#> v) = (a <*> b) <#> v
310+||| + Field unity is the identity element of scalar multiplication:
308−||| forall a, unity <*> a == a
311+||| forall v, unity <#> v = v
309−||| + Distributivity of `<*>` and `<+>`:
312+||| + Distributivity of `<#>` and `<+>`:
310−||| forall a x y, a <*> (x <+> y) == (a <*> x) <+> (a <*> y)
313+||| forall a v w, a <#> (v <+> w) == (a <#> v) <+> (a <#> w)
311−||| forall a b x, (a <+> b) <*> x == (a <*> x) <+> (b <*> x)
314+||| forall a b v, (a <+> b) <#> v == (a <#> v) <+> (b <#> v)
312−class (Field a, AbelianGroup a) => VectorSpace a a where {}
315+class (Field a, AbelianGroup b) => VectorSpace a b where
313−
316+ (<#>) : a -> b -> b
314−class (VerifiedField a, VerifiedAbelianGroup a, VectorSpace a a) => VerifiedVectorSpace a a where
318+class (VerifiedField a, VerifiedAbelianGroup b, VectorSpace a b) => VerifiedVectorSpace a b where
315− total vectorspaceScalarUnityIsUnityL : (l : a) -> l <*> unity = l
319+ total vectorspaceScalarMultiplyComposition : (x,y : a) -> (v : b) -> x <#> (y <#> v) = (x <*> y) <#> v
316− total vectorspaceScalarUnityIsUnityR : (r : a) -> unity <*> r = r
320+ total vectorspaceScalarUnityIsUnity : (v : b) -> unity <#> v = v
317− total vectorspaceScalarIsDistributiveWRTVectorAddition : (s : a) -> (x, y : a) -> s <*> (x <+> y) = (s <*> x) <+> (s <*> y)
321+ total vectorspaceScalarMultDistributiveWRTVectorAddition : (s : a) -> (v, w : b) -> s <#> (v <+> w) = (s <#> v) <+> (s <#> w)
318− total vectorspaceScalarIsDistributiveWRTFieldAddition : (s, t : a) -> (x : a) -> (s <+> t) <*> x = (s <*> x) <+> (t <*> x)
322+ total vectorspaceScalarMultDistributiveWRTFieldAddition : (s, t : a) -> (v : b) -> (s <+> t) <#> v = (s <#> v) <+> (t <#> v)
321-- XXX todo:
324-- XXX todo:
322-- Structures where "abs" make sense.
325-- Structures where "abs" make sense.