In [1]:

```
import proveit
# Prepare this notebook for defining the axioms of a theory:
%axioms_notebook # Keep this at the top following 'import proveit'.
from proveit import Function
from proveit import m, n, v, x, y, A, B, K, S, T, V, W
from proveit.core_expr_types import a_i, v_i, a_1_to_n, x_1_to_n, A_1_to_m
from proveit.logic import (And, Iff, Equals, Forall, Exists, Set,
InSet, NotInSet)
from proveit.numbers import one, Add, NaturalPos, Interval
from proveit.linear_algebra import lin_comb_axn, some_nonzero_a
from proveit.linear_algebra import (LinMap, LinMapAdd,
VecAdd, ScalarMult,
VecSpaces, SpanningSets, Bases,
VecZero, LinDepSets,
TensorProd, TensorExp)
```

In [2]:

```
%begin axioms
```

TODO: We need axioms to define vectors spaces (over fields and for specific vector addition and scalar multiplication operators to be fully abstract; alternatively, we could use the normal addition and multiplication operators and use literal generalization to be more general). We then define a LinMap according to its properties (see lin_map_domains and lin_map_linearity in the theorems).

Define the addition of linear maps.

In [3]:

```
linear_map_unary_addition = Forall(
(V, W), Forall(S, Equals(LinMapAdd(S), S),
domain=LinMap(V, W)))
```

In [4]:

```
linear_map_binary_addition = Forall(
(V, W), Forall((S, T),
Forall(v, Equals(Function(LinMapAdd(S, T), v),
Add(Function(S, v),
Function(T, v))),
domain=V),
domain=LinMap(V, W)))
```

In [5]:

```
linear_map_multi_addition = Forall(
m, Forall((A_1_to_m, B),
Equals(LinMapAdd(A_1_to_m, B),
LinMapAdd(LinMapAdd(A_1_to_m), B)).with_wrap_after_operator()),
domain=NaturalPos)
```

In [6]:

```
tensor_exp_one = Forall(x, Equals(TensorExp(x, one), x))
```

In [7]:

```
%end axioms
```