# Relation LINEAR-SPACE

## Slots on this relation:

Documentation:
Abstract linear or vector space of arbitrary dimension. Defines operations on vectors over a scalar field.
Arity: 7

## Axioms:

```(Nth-Domain Linear-Space 2 Class)

(Nth-Domain Linear-Space 1 Class)

(<=> (Linear-Space ?Scalar-Domain
?Vector-Domain
?S-Zero
?S-One
?V-Zero
?Mult
(And (Class ?Scalar-Domain)
(Class ?Vector-Domain)
(Field ?Scalar-Domain ?Add ?S-Zero ?Mult ?S-One)
(Forall (?S ?V)
(=> (And (Instance-Of ?S ?Scalar-Domain)
(Instance-Of ?V ?Vector-Domain))
(Instance-Of (Value ?Mult ?S ?V)
?Vector-Domain)))
(Forall (?S ?V1 ?V2)
(=> (And (Instance-Of ?S ?Scalar-Domain)
(Instance-Of ?V1 ?Vector-Domain)
(Instance-Of ?V2 ?Vector-Domain))
(= (Value ?Mult ?S (Value ?Add ?V1 ?V2))
(Value ?Mult ?S ?V1)
(Value ?Mult ?S ?V2)))))
(Forall (?S1 ?S2 ?V)
(=> (And (Instance-Of ?S1 ?Scalar-Domain)
(Instance-Of ?S2 ?Scalar-Domain)
(Instance-Of ?V ?Vector-Domain))
(= (Value ?Mult (Value ?Add ?S1 ?S2) ?V)
(Value ?Mult ?S1 ?V)
(Value ?Mult ?S2 ?V)))))
(Forall (?S1 ?S2 ?V)
(=> (And (Instance-Of ?S1 ?Scalar-Domain)
(Instance-Of ?S2 ?Scalar-Domain)
(Instance-Of ?V ?Vector-Domain))
(= (Value ?Mult (Value ?Mult ?S1 ?S2) ?V)
(Value ?Mult ?S1 (Value ?Mult ?S2 ?V)))))
(Forall (?V)
(=> (Instance-Of ?V ?Vector-Domain)
(And (= (Value ?Mult ?S-One ?V) ?V)
(= (Value ?Mult ?S-Zero ?V) ?V-Zero))))))

```