logo
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
Defining axioms for theory 'proveit.linear_algebra.scalar_multiplication'
Subsequent end-of-cell assignments will define axioms
%end_axioms will finalize the definitions

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))
Out[3]:
scalar_mult_extends_number_mult:
In [4]:
%end axioms
These axioms may now be imported from the theory package: proveit.linear_algebra.scalar_multiplication