Theory of proveit.linear_algebra

Provide description here.

import proveit
%theory # toggles between interactive and static modes

Local content of this theory

common expressions	axioms	theorems	demonstrations

Sub-theories

addition	addition of vectors
negation	negation (additive inverse) of vectors
scalar_multiplication	scalar multiplication of vectors
inner_products	inner product spaces and inner products
vector_sets	Spanning set, linear dependence, and bases
linear_maps	linear maps from vector space to vector space
matrices	matrix representations of linear maps over finite vector spaces
tensors	tensor products and generalization of matrices
lie_algebra	Lie algebra and Lie group concepts and notation

All axioms contained within this theory

proveit.linear_algebra.linear_map_unary_addition

proveit.linear_algebra.linear_map_binary_addition

proveit.linear_algebra.linear_map_multi_addition

proveit.linear_algebra.tensor_exp_one

proveit.linear_algebra.addition

proveit.linear_algebra.addition.scalar_add_extends_number_add

proveit.linear_algebra.addition.scalar_sum_extends_number_sum

proveit.linear_algebra.addition.vec_sum_single

proveit.linear_algebra.addition.vec_sum_split_last

proveit.linear_algebra.negation

This sub-theory contains no axioms.

proveit.linear_algebra.scalar_multiplication

proveit.linear_algebra.scalar_multiplication.scalar_mult_extends_number_mult

proveit.linear_algebra.inner_products

proveit.linear_algebra.inner_products.inner_prod_space_def

proveit.linear_algebra.inner_products.hilbert_space_def

proveit.linear_algebra.inner_products.norm_def

proveit.linear_algebra.inner_products.ortho_norm_bases_def

proveit.linear_algebra.inner_products.ortho_proj_def

proveit.linear_algebra.vector_sets

proveit.linear_algebra.vector_sets.span_def

proveit.linear_algebra.vector_sets.spanning_set_def

proveit.linear_algebra.vector_sets.lindep_set_def

proveit.linear_algebra.vector_sets.bases_def

proveit.linear_algebra.vector_sets.dim_def

proveit.linear_algebra.linear_maps

proveit.linear_algebra.linear_maps.lin_map_def

proveit.linear_algebra.linear_maps.vec_add_lin_map

proveit.linear_algebra.linear_maps.scalar_mult_lin_map

proveit.linear_algebra.linear_maps.identity_def

proveit.linear_algebra.linear_maps.commutator_def

proveit.linear_algebra.linear_maps.anti_commutator_def

proveit.linear_algebra.matrices

This sub-theory contains no axioms.

proveit.linear_algebra.tensors

proveit.linear_algebra.tensors.unary_tensor_prod_def

proveit.linear_algebra.tensors.tensor_prod_in_vec_space_only_if_valid

proveit.linear_algebra.tensors.multi_tensor_prod_def

proveit.linear_algebra.lie_algebra

This sub-theory contains no axioms.