#import "../cfg.typ": cfg
#show: cfg

= Vector spaces
$(V, +, dot)$ is a vector space over a field $F :=$
+ $(V, +)$ is an abelian group.
+ $dot in V^(F times V)$.
+ $V$ is closed under $dot$.
+ $lambda(a + b) = lambda a + lambda b$.
+ $(lambda + mu)a = lambda a + mu a$. 
+ $(lambda mu)a = lambda (mu a)$.
+ $1a = a$.

A linear combination of vectors $a_1, ..., a_n := sum_i lambda_i a_i$.

A system of vectors $:=$ sequence of the vectors.

b is linerly expressed through vectors $a_1, ..., a_n :=$ it's their linear combination. 

A system of vectors $e_1, e_2, ..., e_n$ is a basis of a vector space $V :=$
+ ${e_1, e_2, ..., e_n} subset.eq V$.
+ $exists!$ linear expression of a vector $v$ through $e_1, ..., e_n$.

Coordinates of a vector $v$ in a basis $e_1, e_2, ..., e_n :=$
coefficients of a linear expression of $v$ through $e_1, e_2, ..., e_n$.

A vector space with a basis of $n$ vectors $tilde.eq F^n$.

A dimension of a vector space $:= hash$ its basis vectors. 

A linear combination is trivial $:=$ the coefficients are zero.

Vectors $a_1, ..., a_n$ are linearly dependent $:=
exists$ zero nontrivial linear combination.

A vector $b$ is linearly expressed through vectors $a_1, ..., a_n ->
("the expression is unique" <-> a_1, ..., a_n "are linerly indepndent")$.

A span of a set $S :=
angle.l S angle.r :=$
a set of finite linear combinations of vectors $in S$.

A vector space $V$ is generated by a set $S := V = angle.l S angle.r$.

A vector space is finite-dimensional $:=$ it's generated by a finite set of vectors.

A linear independent system of vectors generating a space is a basis of the space.

A finite-dimensional vector space has a basis.

Bases of a finite-dimensional vector space have the same $\#$ vectors.

Two finite-dimensional vector spaces are isomorphic $<->$ they have the same dimension.

A rank of a system of vectors $:=$ its span dimension.

A system of vectors $a_1, ..., a_n$ is equivalent to a system of vectors
  $b_1, ..., b_n :=
angle.l a_1, ..., a_n angle.r = angle.l b_1, ..., b_n angle.r$. 

$a_1, ..., a_n$ is lenearly expressed through $b_1, ..., b_m$ and vice versa $<->
angle.l a_1, ..., a_n angle.r = angle.l b_1, ..., b_m angle.r$.
