Axioms for the theory of proveit.linear_algebra¶

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
from proveit import m, n, v, x, y, A, B, K, S, T, V, W
from proveit.core_expr_types import a_i, v_i, a_1_to_n, x_1_to_n, A_1_to_m
from proveit.logic import (And, Iff, Equals, Forall, Exists, Set,
InSet, NotInSet)
from proveit.numbers import one, Add, NaturalPos, Interval
from proveit.linear_algebra import lin_comb_axn, some_nonzero_a
from proveit.linear_algebra import (LinMap, LinMapAdd,
VecSpaces, SpanningSets, Bases,
VecZero, LinDepSets,
TensorProd, TensorExp)

In [2]:
%begin axioms

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


TODO: We need axioms to define vectors spaces (over fields and for specific vector addition and scalar multiplication operators to be fully abstract; alternatively, we could use the normal addition and multiplication operators and use literal generalization to be more general). We then define a LinMap according to its properties (see lin_map_domains and lin_map_linearity in the theorems).

Define the addition of linear maps.

In [3]:
linear_map_unary_addition = Forall(
(V, W), Forall(S, Equals(LinMapAdd(S), S),
domain=LinMap(V, W)))

In [4]:
linear_map_binary_addition = Forall(
(V, W), Forall((S, T),
Forall(v, Equals(Function(LinMapAdd(S, T), v),
Function(T, v))),
domain=V),
domain=LinMap(V, W)))

In [5]:
linear_map_multi_addition = Forall(
m, Forall((A_1_to_m, B),

tensor_exp_one = Forall(x, Equals(TensorExp(x, one), x))

%end axioms

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