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 a, b
from proveit.logic import Forall, Equals
from proveit.numbers import Mult, Complex
from proveit.linear_algebra import ScalarMult
```

In [2]:

```
%begin axioms
```

Scalar multiplication and number multiplication are the same when applied to complex numbers:

In [3]:

```
scalar_mult_extends_number_mult = (
Forall((a, b),
Equals(ScalarMult(a, b), Mult(a, b)),
domain=Complex))
```

In [4]:

```
%end axioms
```