Axioms for the theory of proveit.linear_algebra.scalar_multiplication

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

%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:

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

scalar_mult_extends_number_mult:

%end axioms

These axioms may now be imported from the theory package: proveit.linear_algebra.scalar_multiplication