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 m, A, B, K, U, V, W
from proveit.core_expr_types import A_1_to_m
from proveit.logic import And, Forall, Exists, Equals, InSet
from proveit.numbers import Natural
from proveit.linear_algebra import VecSpaces, TensorProd
```

In [2]:

```
%begin axioms
```

A unary tensor product of a vector (over any field) is just the vector itself.

In [3]:

```
unary_tensor_prod_def = Forall(
K, Forall(V, Forall(A, Equals(TensorProd(A), A), domain=V),
domain=VecSpaces(K)))
```

Need binary_tensor_prod_def to really define tensor products

By the following axiom, we can know that a TensorProd only results in an element of a vector space over a field if the operands are also in vector spaces over that field (otherwise, if no such field or vector spaces exists, the TensorProd is not defined unless it is a tensor product of vector spaces themselves):

In [4]:

```
tensor_prod_in_vec_space_only_if_valid = Forall(
K, Forall(
W, Forall(
(A, B), Exists((U, V),
And(InSet(A, U), InSet(B, V)),
domain=VecSpaces(K)),
condition=InSet(TensorProd(A, B), W)),
domain=VecSpaces(K)))
```

We define multiple tensor products as successive tensor products without any constraints for simplicity.

In [5]:

```
multi_tensor_prod_def = \
Forall(m, Forall((A_1_to_m, B),
Equals(TensorProd(A_1_to_m, B),
TensorProd(TensorProd(A_1_to_m), B))
.with_wrap_after_operator()),
domain=Natural)
```

In [6]:

```
%end axioms
```