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