This file defines linear independence in a module or vector space.
It is inspired by Isabelle/HOL's linear algebra, and hence indirectly by HOL Light.
linear_independent R v as
ker (finsupp.total ι M R v) = ⊥. Here
finsupp.total is the
linear map sending a function
f : ι →₀ R with finite support to the linear combination of vectors
v with these coefficients. Then we prove that several other statements are equivalent to this
one, including injectivity of
finsupp.total ι M R v and some versions with explicitly written
All definitions are given for families of vectors, i.e.
v : ι → M where
M is the module or
vector space and
ι : Type* is an arbitrary indexing type.
linear_independent R vstates that the elements of the family
vare linearly independent.
linear_independent.repr hv xreturns the linear combination representing
x : span R (range v)on the linearly independent vectors
hv : linear_independent R v(using classical choice).
linear_independent.repr hvis provided as a linear map.
We prove several specialized tests for linear independence of families of vectors and of sets of vectors.
ιis a finite type, then any function
f : ι → Rhas finite support, so we can reformulate the statement using
∑ i : ι, f i • v iinstead of a sum over an auxiliary
s : finset ι;
linear_independent_empty_type: a family indexed by an empty type is linearly independent;
ιis a singleton, then
linear_independent K vis equivalent to
v (default ι) ≠ 0;
,linear_independent_fin_succ`: type-specific tests for linear independence of families of vector fields;
linear_independent_singleton: linear independence tests for set operations.
In many cases we additionally provide dot-style operations (e.g.,
make the linear independence tests usable as
hv.insert ha etc.
We also prove that any family of vectors includes a linear independent subfamily spanning the same submodule.
We use families instead of sets because it allows us to say that two identical vectors are linearly dependent.
linearly dependent, linear dependence, linearly independent, linear independence
A subfamily of a linearly independent family (i.e., a composition with an injective map) is a linearly independent family.
v is a linearly independent family of vectors and the kernel of a linear map
disjoint with the sumodule spaned by the vectors of
f ∘ v is a linearly independent
family of vectors. See also
linear_independent.map' for a special case assuming
ker f = ⊥.
An injective linear map sends linearly independent families of vectors to linearly independent
families of vectors. See also
linear_independent.map for a more general statement.
If the image of a family of vectors under a linear map is linearly independent, then so is the original family.
f is an injective linear map, then the family
f ∘ v is linearly independent
if and only if the family
v is linearly independent.
The following lemmas use the subtype defined by a set in
M as the index set
Canonical isomorphism between linear combinations and the span of linearly independent vectors.
Linear combination representing a vector in the span of linearly independent vectors.
Given a family of linearly independent vectors, we can represent any vector in their span as
a linear combination of these vectors. These are provided by this linear map.
It is simply one direction of