# Theorems (or conjectures) for the theory of proveit.linear_algebra¶

In [1]:
import proveit
# Prepare this notebook for defining the theorems of a theory:
%theorems_notebook # Keep this at the top following 'import proveit'.

from proveit import n
from proveit.logic import Forall, InSet, CartExp, InClass
from proveit.numbers import NaturalPos, Rational, Real, Complex
from proveit.linear_algebra import VecSpaces

In [2]:
%begin theorems

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


Number field vector sets are vector spaces:

In [3]:
rational_vec_set_is_vec_space = Forall(
n, InClass(CartExp(Rational, n), VecSpaces(Rational)),
domain = NaturalPos)

rational_vec_set_is_vec_space (conjecture without proof):

In [4]:
real_vec_set_is_vec_space = Forall(
n, InClass(CartExp(Real, n), VecSpaces(Real)),
domain = NaturalPos)

real_vec_set_is_vec_space (conjecture without proof):

In [5]:
complex_vec_set_is_vec_space = Forall(
n, InClass(CartExp(Complex, n), VecSpaces(Complex)),
domain = NaturalPos)

complex_vec_set_is_vec_space (conjecture without proof):

As special cases, number fields are also vector spaces:

In [6]:
rational_set_is_vec_space = InClass(Rational, VecSpaces(Rational))

rational_set_is_vec_space (conjecture without proof):

In [7]:
real_set_is_vec_space = InClass(Real, VecSpaces(Real))

real_set_is_vec_space (conjecture without proof):

In [8]:
complex_set_is_vec_space = InClass(Complex, VecSpaces(Complex))

complex_set_is_vec_space (conjecture without proof):

In [9]:
%end theorems

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