VectorSpace concept

Description

A vector space is an algebraic structure over a Field of values. It is an AdditiveAbeleanGroup and has a scalar multiplication that satisfies following axioms:

The vector-space is closed under scalar multiplication: av is an element of the vector-space.
Scalar multiplication is associative: a(bv) = (ab)v.
1 v = v where 1 denotes the multiplicative identity.
Scalar multiplication distributes over vector addition: a(v+w) = av + aw
Vector multiplication distributes over scalar addition: (a+b)v = av + bv

Refinement of

AdditiveAbeleanGroup.

Associated types

Next to those of AdditiveAbeleanGroup:

value_type: Field over which the vector space is defined

Notation

`X`	A type that is a model of VectorSpace
`v,w`	Object of type `X`
`a,b`	object of type convertible to `X::value_type`
0	zero vector, i.e. the identity for the addition
`0`	zero scalar, i.e. the identity for the addition in the Field `X::value_type`
1	multiplicative identity in the field over which the vector-space is defined.

Definitions

Valid expressions

In addition to those defined by AdditiveAbelianGroup:

Name	Expression	Return type
Scalar multiplication	`a * v`	`X`
Scalar division	`v / a`	`X`
Scalar multiplication	`v *= a`	`X`
Scalar division	`v /= a`	`X`

Expression semantics

Name	Expression	Precondition	Semantics
Scalar multiplication	a*v
Scalar division	v / a	a!=0	equivalent to `(1/a) * v`
Scalar multiplication	v*=a		v=a*v
Scalar division	v/=a	a!=0	v=v/a

Complexity guarantees

Invariants

In addition to those of AdditiveAbelianGroup:

Multiplicative identity	`1 v = v`
Scalar multiplication distributes over vector addition	`a(v+w) = av + aw`
Vector multiplication distributes over scalar addition	`(a+b)v = av + bv`
Negation	`-v = (-1)*v`