# Axioms for the theory of proveit.linear_algebra.linear_maps¶

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, Lambda, Conditional
from proveit import c, x, A, B, P, V, W
from proveit.logic import Forall, Equals, InSet
from proveit.linear_algebra import (
VecSpaces, LinMap, VecAdd, ScalarMult)

In [2]:
%begin axioms

Defining axioms for theory 'proveit.linear_algebra.linear_maps'
Subsequent end-of-cell assignments will define axioms
%end_axioms will finalize the definitions

In [ ]:


In [ ]:



### Define vector addition and scalar multiplication on LinMaps¶

In [3]:
vec_add_lin_map = Forall(
(V, W), Forall(
(A, B), Equals(VecAdd(A, B),
Lambda(x, Conditional(
Function(B, x)),
InSet(x, V)))),
domain=LinMap(V, W)))

Out[3]:
In [4]:
scalar_mult_lin_map = Forall(
(V, W), Forall(
(c, P), Equals(ScalarMult(c, P),
Lambda(x, Conditional(
ScalarMult(c, Function(P, x)),
InSet(x, V)))),
domain=LinMap(V, W)))

Out[4]:
scalar_mult_lin_map:
In [5]:
%end axioms

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