# 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, Composition
from proveit import c, x, y, A, B, K, P, V, W, Px, Py
from proveit.logic import And, Iff, Forall, Equals, InSet
from proveit.linear_algebra import (
VecSpaces, LinMap, VecAdd, vec_subtract, ScalarMult, VecZero, Identity, Commutator, AntiCommutator)

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


### A linear map is a map with linear properties¶

In [3]:
lin_map_def = Forall(
K, Forall(
(V, W), Forall(
P, Iff(InSet(P, LinMap(V, W)),
And(Forall(x, InSet(Px, W), domain=V),
domain=V),
Forall(c, Forall(x, Equals(Function(P, ScalarMult(c, x)),
ScalarMult(c, Px)),
domain=V),
domain=K)).with_wrapping_at(2, 4)).with_wrap_after_operator()),
domain=VecSpaces(K)))

lin_map_def:

### A linear map is, itself, a vector space¶

by defining vector addition and scalar addition on a linear map in the following manner.

In [4]:
vec_add_lin_map = Forall(
K, Forall(
(V, W), Forall(
Lambda(x, Conditional(
Function(B, x)),
InSet(x, V)))),
domain=LinMap(V, W)),
domain=VecSpaces(K)))

In [5]:
scalar_mult_lin_map = Forall(
K, Forall(
(V, W), Forall(
c, Forall(
P, Equals(ScalarMult(c, P),
Lambda(x, Conditional(ScalarMult(c, Function(P, x)),
InSet(x, V)))),
domain=LinMap(V, W)),
domain=K),
domain=VecSpaces(K)))

scalar_mult_lin_map:
In [6]:
identity_def = Forall(V, Equals(Identity(V), Lambda(x, Conditional(x, InSet(x, V)))))

identity_def:

### Commutator and Anti-commutator¶

In [7]:
commutator_def = Forall(
K, Forall(
V, Forall((A, B), Equals(Commutator(A, B), vec_subtract(Composition(A, B), Composition(B, A))),
domain=V),
domain=VecSpaces(K)))

commutator_def:
In [8]:
anti_commutator_def = Forall(
K, Forall(
V, Forall((A, B), Equals(AntiCommutator(A, B), VecAdd(Composition(A, B), Composition(B, A))),
domain=V),
domain=VecSpaces(K)))

anti_commutator_def:
In [9]:
%end axioms

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