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

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

%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:

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):

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):

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:

rational_set_is_vec_space = InClass(Rational, VecSpaces(Rational))

rational_set_is_vec_space (conjecture without proof):

real_set_is_vec_space = InClass(Real, VecSpaces(Real))

real_set_is_vec_space (conjecture without proof):

complex_set_is_vec_space = InClass(Complex, VecSpaces(Complex))

complex_set_is_vec_space (conjecture without proof):

%end theorems

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