# Linear independence and bases

This file defines linear independence and bases in a module or vector space.

It is inspired by Isabelle/HOL's linear algebra, and hence indirectly by HOL Light.

## Main definitions

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 v states that the elements of the family v are linearly independent.

• linear_independent.repr hv x returns the linear combination representing x : span R (range v) on the linearly independent vectors v, given hv : linear_independent R v (using classical choice). linear_independent.repr hv is provided as a linear map.

• is_basis R v states that the vector family v is a basis, i.e. it is linearly independent and spans the entire space.

• is_basis.repr hv x is the basis version of linear_independent.repr hv x. It returns the linear combination representing x : M on a basis v of M (using classical choice). The argument hv must be a proof that is_basis R v. is_basis.repr hv is given as a linear map as well.

• is_basis.constr hv f constructs a linear map M₁ →ₗ[R] M₂ given the values f : ι → M₂ at the basis v : ι → M₁, given hv : is_basis R v.

## Main statements

• is_basis.ext states that two linear maps are equal if they coincide on a basis.

• exists_is_basis states that every vector space has a basis.

## Implementation notes

We use families instead of sets because it allows us to say that two identical vectors are linearly dependent. For bases, this is useful as well because we can easily derive ordered bases by using an ordered index type ι.

If you want to use sets, use the family (λ x, x : s → M) given a set s : set M. The lemmas linear_independent.to_subtype_range and linear_independent.of_subtype_range connect those two worlds.

## Tags

linearly dependent, linear dependence, linearly independent, linear independence, basis

def linear_independent {ι : Type u_1} (R : Type u_3) {M : Type u_5} (v : ι → M) [ring R] [module R M] :
Prop

Linearly independent family of vectors

Equations
theorem linear_independent_iff {ι : Type u_1} {R : Type u_3} {M : Type u_5} {v : ι → M} [ring R] [module R M] :
linear_independent R v ∀ (l : ι →₀ R), (finsupp.total ι M R v) l = 0 → l = 0

theorem linear_independent_iff' {ι : Type u_1} {R : Type u_3} {M : Type u_5} {v : ι → M} [ring R] [module R M] :
linear_independent R v ∀ (s : finset ι) (g : ι → R), s.sum (λ (i : ι), g i v i) = 0 → ∀ (i : ι), i s → g i = 0

theorem linear_independent_empty_type {ι : Type u_1} {R : Type u_3} {M : Type u_5} {v : ι → M} [ring R] [module R M] :

theorem linear_independent.ne_zero {ι : Type u_1} {R : Type u_3} {M : Type u_5} {v : ι → M} [ring R] [module R M] {i : ι} :
0 1 → linear_independent R v → v i 0

theorem linear_independent.comp {ι : Type u_1} {ι' : Type u_2} {R : Type u_3} {M : Type u_5} {v : ι → M} [ring R] [module R M] (h : linear_independent R v) (f : ι' → ι) :

theorem linear_independent_of_zero_eq_one {ι : Type u_1} {R : Type u_3} {M : Type u_5} {v : ι → M} [ring R] [module R M] :
0 = 1 → linear_independent R v

theorem linear_independent.unique {ι : Type u_1} {R : Type u_3} {M : Type u_5} {v : ι → M} [ring R] [module R M] (hv : linear_independent R v) {l₁ l₂ : ι →₀ R} :
(finsupp.total ι M R v) l₁ = (finsupp.total ι M R v) l₂ → l₁ = l₂

theorem linear_independent.injective {ι : Type u_1} {R : Type u_3} {M : Type u_5} {v : ι → M} [ring R] [module R M] :

theorem linear_independent_span {ι : Type u_1} {R : Type u_3} {M : Type u_5} {v : ι → M} [ring R] [module R M] :
linear_independent R v → linear_independent R (λ (i : ι), v i, _⟩)

The following lemmas use the subtype defined by a set in M as the index set ι.

theorem linear_independent_comp_subtype {ι : Type u_1} {R : Type u_3} {M : Type u_5} {v : ι → M} [ring R] [module R M] {s : set ι} :
linear_independent R (v subtype.val) ∀ (l : ι →₀ R), l finsupp.supported R R s → (finsupp.total ι M R v) l = 0 → l = 0

theorem linear_independent_subtype {R : Type u_3} {M : Type u_5} [ring R] [module R M] {s : set M} :
linear_independent R (λ (x : s), x) ∀ (l : M →₀ R), l finsupp.supported R R s → (finsupp.total M M R id) l = 0 → l = 0

theorem linear_independent_comp_subtype_disjoint {ι : Type u_1} {R : Type u_3} {M : Type u_5} {v : ι → M} [ring R] [module R M] {s : set ι} :

theorem linear_independent_subtype_disjoint {R : Type u_3} {M : Type u_5} [ring R] [module R M] {s : set M} :

theorem linear_independent_iff_total_on {R : Type u_3} {M : Type u_5} [ring R] [module R M] {s : set M} :

theorem linear_independent.to_subtype_range {ι : Type u_1} {R : Type u_3} {M : Type u_5} {v : ι → M} [ring R] [module R M] :

theorem linear_independent.of_subtype_range {ι : Type u_1} {R : Type u_3} {M : Type u_5} {v : ι → M} [ring R] [module R M] :

theorem linear_independent.restrict_of_comp_subtype {ι : Type u_1} {R : Type u_3} {M : Type u_5} {v : ι → M} [ring R] [module R M] {s : set ι} :

theorem linear_independent_empty {R : Type u_3} {M : Type u_5} [ring R] [module R M] :

theorem linear_independent.mono {R : Type u_3} {M : Type u_5} [ring R] [module R M] {t s : set M} :
t s → linear_independent R (λ (x : s), x) → linear_independent R (λ (x : t), x)

theorem linear_independent.union {R : Type u_3} {M : Type u_5} [ring R] [module R M] {s t : set M} :
linear_independent R (λ (x : s), x) → linear_independent R (λ (x : t), x) → disjoint (submodule.span R s) (submodule.span R t) → linear_independent R (λ (x : (s t)), x)

theorem linear_independent_of_finite {R : Type u_3} {M : Type u_5} [ring R] [module R M] (s : set M) :
(∀ (t : set M), t s → t.finitelinear_independent R (λ (x : t), x)) → linear_independent R (λ (x : s), x)

theorem linear_independent_Union_of_directed {R : Type u_3} {M : Type u_5} [ring R] [module R M] {η : Type u_1} {s : η → set M} :
directed has_subset.subset s → (∀ (i : η), linear_independent R (λ (x : (s i)), x)) → linear_independent R (λ (x : ⋃ (i : η), s i), x)

theorem linear_independent_sUnion_of_directed {R : Type u_3} {M : Type u_5} [ring R] [module R M] {s : set (set M)} :
directed_on has_subset.subset s → (∀ (a : set M), a s → linear_independent R (λ (x : a), x)) → linear_independent R (λ (x : ⋃₀s), x)

theorem linear_independent_bUnion_of_directed {R : Type u_3} {M : Type u_5} [ring R] [module R M] {η : Type u_1} {s : set η} {t : η → set M} :
directed_on (t ⁻¹'o has_subset.subset) s → (∀ (a : η), a s → linear_independent R (λ (x : (t a)), x)) → linear_independent R (λ (x : ⋃ (a : η) (H : a s), t a), x)

theorem linear_independent_Union_finite_subtype {R : Type u_3} {M : Type u_5} [ring R] [module R M] {ι : Type u_1} {f : ι → set M} :
(∀ (i : ι), linear_independent R (λ (x : (f i)), x)) → (∀ (i : ι) (t : set ι), t.finite → i t → disjoint (submodule.span R (f i)) (⨆ (i : ι) (H : i t), submodule.span R (f i))) → linear_independent R (λ (x : ⋃ (i : ι), f i), x)

theorem linear_independent_Union_finite {R : Type u_3} {M : Type u_5} [ring R] [module R M] {η : Type u_1} {ιs : η → Type u_2} {f : Π (j : η), ιs j → M} :
(∀ (j : η), linear_independent R (f j)) → (∀ (i : η) (t : set η), t.finite → i t → disjoint (submodule.span R (set.range (f i))) (⨆ (i : η) (H : i t), submodule.span R (set.range (f i)))) → linear_independent R (λ (ji : Σ (j : η), ιs j), f ji.fst ji.snd)

def linear_independent.total_equiv {ι : Type u_1} {R : Type u_3} {M : Type u_5} {v : ι → M} [ring R] [module R M] :

Canonical isomorphism between linear combinations and the span of linearly independent vectors.

Equations
def linear_independent.repr {ι : Type u_1} {R : Type u_3} {M : Type u_5} {v : ι → M} [ring R] [module R M] :

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 linear_independent.total_equiv.

Equations
theorem linear_independent.total_repr {ι : Type u_1} {R : Type u_3} {M : Type u_5} {v : ι → M} [ring R] [module R M] (hv : linear_independent R v) (x : (submodule.span R (set.range v))) :
(finsupp.total ι M R v) ((hv.repr) x) = x

theorem linear_independent.total_comp_repr {ι : Type u_1} {R : Type u_3} {M : Type u_5} {v : ι → M} [ring R] [module R M] (hv : linear_independent R v) :

theorem linear_independent.repr_ker {ι : Type u_1} {R : Type u_3} {M : Type u_5} {v : ι → M} [ring R] [module R M] (hv : linear_independent R v) :

theorem linear_independent.repr_range {ι : Type u_1} {R : Type u_3} {M : Type u_5} {v : ι → M} [ring R] [module R M] (hv : linear_independent R v) :

theorem linear_independent.repr_eq {ι : Type u_1} {R : Type u_3} {M : Type u_5} {v : ι → M} [ring R] [module R M] (hv : linear_independent R v) {l : ι →₀ R} {x : (submodule.span R (set.range v))} :
(finsupp.total ι M R v) l = x → (hv.repr) x = l

theorem linear_independent.repr_eq_single {ι : Type u_1} {R : Type u_3} {M : Type u_5} {v : ι → M} [ring R] [module R M] (hv : linear_independent R v) (i : ι) (x : (submodule.span R (set.range v))) :
x = v i → (hv.repr) x = finsupp.single i 1

theorem linear_independent_iff_not_smul_mem_span {ι : Type u_1} {R : Type u_3} {M : Type u_5} {v : ι → M} [ring R] [module R M] :
linear_independent R v ∀ (i : ι) (a : R), a v i submodule.span R (v '' (set.univ \ {i})) → a = 0

theorem surjective_of_linear_independent_of_span {ι : Type u_1} {ι' : Type u_2} {R : Type u_3} {M : Type u_5} {v : ι → M} [ring R] [module R M] (hv : linear_independent R v) (f : ι' ι) :

theorem eq_of_linear_independent_of_span_subtype {R : Type u_3} {M : Type u_5} [ring R] [module R M] {s t : set M} :
0 1 → linear_independent R (λ (x : s), x) → t s → s (submodule.span R t) → s = t

theorem linear_independent.image {ι : Type u_1} {R : Type u_3} {M : Type u_5} {M' : Type u_6} {v : ι → M} [ring R] [add_comm_group M'] [module R M] [module R M'] (hv : linear_independent R v) {f : M →ₗ[R] M'} :

theorem linear_independent.image_subtype {R : Type u_3} {M : Type u_5} {M' : Type u_6} [ring R] [add_comm_group M'] [module R M] [module R M'] {s : set M} {f : M →ₗ[R] M'} :
linear_independent R (λ (x : s), x) → disjoint (submodule.span R s) f.kerlinear_independent R (λ (x : (f '' s)), x)

theorem linear_independent.inl_union_inr {R : Type u_3} {M : Type u_5} {M' : Type u_6} [ring R] [add_comm_group M'] [module R M] [module R M'] {s : set M} {t : set M'} :
linear_independent R (λ (x : s), x) → linear_independent R (λ (x : t), x) → linear_independent R (λ (x : ((linear_map.inl R M M') '' s (linear_map.inr R M M') '' t)), x)

theorem linear_independent_inl_union_inr' {ι : Type u_1} {ι' : Type u_2} {R : Type u_3} {M : Type u_5} {M' : Type u_6} [ring R] [add_comm_group M'] [module R M] [module R M'] {v : ι → M} {v' : ι' → M'} :

theorem linear_independent_monoid_hom (G : Type u_1) [monoid G] (L : Type u_2) :
linear_independent L (λ (f : G →* L), f)

Dedekind's linear independence of characters

theorem le_of_span_le_span {R : Type u_3} {M : Type u_5} [ring R] [module R M] {s t u : set M} :
0 1 → linear_independent R subtype.val → s u → t u → submodule.span R s submodule.span R t → s t

theorem span_le_span_iff {R : Type u_3} {M : Type u_5} [ring R] [module R M] {s t u : set M} :
0 1 → linear_independent R subtype.val → s u → t u → (submodule.span R s submodule.span R t s t)

def is_basis {ι : Type u_1} (R : Type u_3) {M : Type u_5} (v : ι → M) [ring R] [module R M] :
Prop

A family of vectors is a basis if it is linearly independent and all vectors are in the span.

Equations
theorem is_basis.mem_span {ι : Type u_1} {R : Type u_3} {M : Type u_5} {v : ι → M} [ring R] [module R M] (hv : is_basis R v) (x : M) :

theorem is_basis.comp {ι : Type u_1} {ι' : Type u_2} {R : Type u_3} {M : Type u_5} {v : ι → M} [ring R] [module R M] (hv : is_basis R v) (f : ι' → ι) :

theorem is_basis.injective {ι : Type u_1} {R : Type u_3} {M : Type u_5} {v : ι → M} [ring R] [module R M] :
is_basis R v → 0 1 → function.injective v

def is_basis.repr {ι : Type u_1} {R : Type u_3} {M : Type u_5} {v : ι → M} [ring R] [module R M] :
is_basis R v → (M →ₗ[R] ι →₀ R)

Given a basis, any vector can be written as a linear combination of the basis vectors. They are given by this linear map. This is one direction of module_equiv_finsupp.

Equations
theorem is_basis.total_repr {ι : Type u_1} {R : Type u_3} {M : Type u_5} {v : ι → M} [ring R] [module R M] (hv : is_basis R v) (x : M) :
(finsupp.total ι M R v) ((hv.repr) x) = x

theorem is_basis.total_comp_repr {ι : Type u_1} {R : Type u_3} {M : Type u_5} {v : ι → M} [ring R] [module R M] (hv : is_basis R v) :

theorem is_basis.repr_ker {ι : Type u_1} {R : Type u_3} {M : Type u_5} {v : ι → M} [ring R] [module R M] (hv : is_basis R v) :

theorem is_basis.repr_range {ι : Type u_1} {R : Type u_3} {M : Type u_5} {v : ι → M} [ring R] [module R M] (hv : is_basis R v) :

theorem is_basis.repr_total {ι : Type u_1} {R : Type u_3} {M : Type u_5} {v : ι → M} [ring R] [module R M] (hv : is_basis R v) (x : ι →₀ R) :
x finsupp.supported R R set.univ(hv.repr) ((finsupp.total ι M R v) x) = x

theorem is_basis.repr_eq_single {ι : Type u_1} {R : Type u_3} {M : Type u_5} {v : ι → M} [ring R] [module R M] (hv : is_basis R v) {i : ι} :
(hv.repr) (v i) = finsupp.single i 1

def is_basis.constr {ι : Type u_1} {R : Type u_3} {M : Type u_5} {M' : Type u_6} {v : ι → M} [ring R] [add_comm_group M'] [module R M] [module R M'] :
is_basis R v → (ι → M') → (M →ₗ[R] M')

Construct a linear map given the value at the basis.

Equations
theorem is_basis.constr_apply {ι : Type u_1} {R : Type u_3} {M : Type u_5} {M' : Type u_6} {v : ι → M} [ring R] [add_comm_group M'] [module R M] [module R M'] (hv : is_basis R v) (f : ι → M') (x : M) :
(hv.constr f) x = ((hv.repr) x).sum (λ (b : ι) (a : R), a f b)

theorem is_basis.ext {ι : Type u_1} {R : Type u_3} {M : Type u_5} {M' : Type u_6} {v : ι → M} [ring R] [add_comm_group M'] [module R M] [module R M'] {f g : M →ₗ[R] M'} :
is_basis R v → (∀ (i : ι), f (v i) = g (v i)) → f = g

@[simp]
theorem constr_basis {ι : Type u_1} {R : Type u_3} {M : Type u_5} {M' : Type u_6} {v : ι → M} [ring R] [add_comm_group M'] [module R M] [module R M'] {f : ι → M'} {i : ι} (hv : is_basis R v) :
(hv.constr f) (v i) = f i

theorem constr_eq {ι : Type u_1} {R : Type u_3} {M : Type u_5} {M' : Type u_6} {v : ι → M} [ring R] [add_comm_group M'] [module R M] [module R M'] {g : ι → M'} {f : M →ₗ[R] M'} (hv : is_basis R v) :
(∀ (i : ι), g i = f (v i)) → hv.constr g = f

theorem constr_self {ι : Type u_1} {R : Type u_3} {M : Type u_5} {M' : Type u_6} {v : ι → M} [ring R] [add_comm_group M'] [module R M] [module R M'] (hv : is_basis R v) (f : M →ₗ[R] M') :
hv.constr (λ (i : ι), f (v i)) = f

theorem constr_zero {ι : Type u_1} {R : Type u_3} {M : Type u_5} {M' : Type u_6} {v : ι → M} [ring R] [add_comm_group M'] [module R M] [module R M'] (hv : is_basis R v) :
hv.constr (λ (i : ι), 0) = 0

theorem constr_add {ι : Type u_1} {R : Type u_3} {M : Type u_5} {M' : Type u_6} {v : ι → M} [ring R] [add_comm_group M'] [module R M] [module R M'] {g f : ι → M'} (hv : is_basis R v) :
hv.constr (λ (i : ι), f i + g i) = hv.constr f + hv.constr g

theorem constr_neg {ι : Type u_1} {R : Type u_3} {M : Type u_5} {M' : Type u_6} {v : ι → M} [ring R] [add_comm_group M'] [module R M] [module R M'] {f : ι → M'} (hv : is_basis R v) :
hv.constr (λ (i : ι), -f i) = -hv.constr f

theorem constr_sub {ι : Type u_1} {R : Type u_3} {M : Type u_5} {M' : Type u_6} {v : ι → M} [ring R] [add_comm_group M'] [module R M] [module R M'] (hv : is_basis R v) {g f : ι → M'} (hs : is_basis R v) :
hv.constr (λ (i : ι), f i - g i) = hs.constr f - hs.constr g

theorem constr_smul {ι : Type u_1} {R : Type u_2} {M : Type u_3} [comm_ring R] [module R M] {v : ι → R} {f : ι → M} {a : R} (hv : is_basis R v) :
hv.constr (λ (b : ι), a f b) = a hv.constr f

theorem constr_range {ι : Type u_1} {R : Type u_3} {M : Type u_5} {M' : Type u_6} {v : ι → M} [ring R] [add_comm_group M'] [module R M] [module R M'] [nonempty ι] (hv : is_basis R v) {f : ι → M'} :

def module_equiv_finsupp {ι : Type u_1} {R : Type u_3} {M : Type u_5} {v : ι → M} [ring R] [module R M] :
is_basis R v → (M ≃ₗ[R] ι →₀ R)

Canonical equivalence between a module and the linear combinations of basis vectors.

Equations
def equiv_of_is_basis {ι : Type u_1} {ι' : Type u_2} {R : Type u_3} {M : Type u_5} {M' : Type u_6} [ring R] [add_comm_group M'] [module R M] [module R M'] {v : ι → M} {v' : ι' → M'} :
is_basis R v → is_basis R v' → ι ι' → (M ≃ₗ[R] M')

Isomorphism between the two modules, given two modules M and M' with respective bases v and v' and a bijection between the indexing sets of the two bases.

Equations
def equiv_of_is_basis' {ι : Type u_1} {ι' : Type u_2} {R : Type u_3} {M : Type u_5} {M' : Type u_6} [ring R] [add_comm_group M'] [module R M] [module R M'] {v : ι → M} {v' : ι' → M'} (f : M → M') (g : M' → M) :
is_basis R v → is_basis R v' → (∀ (i : ι), f (v i) set.range v') → (∀ (i : ι'), g (v' i) set.range v) → (∀ (i : ι), g (f (v i)) = v i) → (∀ (i : ι'), f (g (v' i)) = v' i) → (M ≃ₗ[R] M')

Isomorphism between the two modules, given two modules M and M' with respective bases v and v' and a bijection between the two bases.

Equations
theorem is_basis_inl_union_inr {ι : Type u_1} {ι' : Type u_2} {R : Type u_3} {M : Type u_5} {M' : Type u_6} [ring R] [add_comm_group M'] [module R M] [module R M'] {v : ι → M} {v' : ι' → M'} :
is_basis R v → is_basis R v' → is_basis R (sum.elim ((linear_map.inl R M M') v) ((linear_map.inr R M M') v'))

theorem is_basis_singleton_one {ι : Type u_1} (R : Type u_2) [unique ι] [ring R] :
is_basis R (λ (_x : ι), 1)

theorem linear_equiv.is_basis {ι : Type u_1} {R : Type u_3} {M : Type u_5} {M' : Type u_6} {v : ι → M} [ring R] [add_comm_group M'] [module R M] [module R M'] (hs : is_basis R v) (f : M ≃ₗ[R] M') :

theorem is_basis_span {ι : Type u_1} {R : Type u_3} {M : Type u_5} {v : ι → M} [ring R] [module R M] :
linear_independent R v → is_basis R (λ (i : ι), v i, _⟩)

theorem is_basis_empty {ι : Type u_1} {R : Type u_3} {M : Type u_5} [ring R] [module R M] :
¬nonempty ι → (∀ (x : M), x = 0) → is_basis R (λ (x : ι), 0)

theorem is_basis_empty_bot {ι : Type u_1} {R : Type u_3} {M : Type u_5} [ring R] [module R M] :
¬nonempty ι → is_basis R (λ (_x : ι), 0)

def equiv_fun_basis {ι : Type u_1} {R : Type u_3} {M : Type u_5} {v : ι → M} [ring R] [module R M] [fintype ι] :
is_basis R v → (M ≃ₗ[R] ι → R)

A module over R with a finite basis is linearly equivalent to functions from its basis to R.

Equations
def module.fintype_of_fintype {ι : Type u_1} {R : Type u_3} {M : Type u_5} {v : ι → M} [ring R] [module R M] [fintype ι] (h : is_basis R v) [fintype R] :

A module over a finite ring that admits a finite basis is finite.

Equations
theorem module.card_fintype {ι : Type u_1} {R : Type u_3} {M : Type u_5} {v : ι → M} [ring R] [module R M] [fintype ι] (h : is_basis R v) [fintype R] [fintype M] :

@[simp]
theorem equiv_fun_basis_symm_apply {ι : Type u_1} {R : Type u_3} {M : Type u_5} {v : ι → M} [ring R] [module R M] [fintype ι] (h : is_basis R v) (x : ι → R) :
((equiv_fun_basis h).symm) x = finset.univ.sum (λ (i : ι), x i v i)

Given a basis v indexed by ι, the canonical linear equivalence between ι → R and M maps a function x : ι → R to the linear combination ∑_i x i • v i.

theorem mem_span_insert_exchange {K : Type u_4} {V : Type u_7} [field K] [vector_space K V] {s : set V} {x y : V} :

theorem linear_independent_iff_not_mem_span {ι : Type u_1} {K : Type u_4} {V : Type u_7} {v : ι → V} [field K] [vector_space K V] :
linear_independent K v ∀ (i : ι), v i submodule.span K (v '' (set.univ \ {i}))

theorem linear_independent_unique {ι : Type u_1} {K : Type u_4} {V : Type u_7} {v : ι → V} [field K] [vector_space K V] [unique ι] :

theorem linear_independent_singleton {K : Type u_4} {V : Type u_7} [field K] [vector_space K V] {x : V} :
x 0 → linear_independent K (λ (x_1 : {x}), x_1)

theorem disjoint_span_singleton {K : Type u_4} {V : Type u_7} [field K] [vector_space K V] {p : submodule K V} {x : V} :
x 0 → (disjoint p (submodule.span K {x}) x p)

theorem linear_independent.insert {K : Type u_4} {V : Type u_7} [field K] [vector_space K V] {s : set V} {x : V} :
linear_independent K (λ (b : s), b) → x submodule.span K s → linear_independent K (λ (b : (has_insert.insert x s)), b)

theorem exists_linear_independent {K : Type u_4} {V : Type u_7} [field K] [vector_space K V] {s t : set V} :
linear_independent K (λ (x : s), x) → s t → (∃ (b : set V) (H : b t), s b t (submodule.span K b) linear_independent K (λ (x : b), x))

theorem exists_subset_is_basis {K : Type u_4} {V : Type u_7} [field K] [vector_space K V] {s : set V} :
linear_independent K (λ (x : s), x) → (∃ (b : set V), s b is_basis K coe)

theorem exists_is_basis (K : Type u_4) (V : Type u_7) [field K] [vector_space K V] :
∃ (b : set V), is_basis K (λ (i : b), i)

theorem exists_of_linear_independent_of_finite_span {K : Type u_4} {V : Type u_7} [field K] [vector_space K V] {s : set V} {t : finset V} :
linear_independent K (λ (x : s), x) → s (submodule.span K t) → (∃ (t' : finset V), t' s t s t' t'.card = t.card)

theorem exists_finite_card_le_of_finite_of_linear_independent_of_span {K : Type u_4} {V : Type u_7} [field K] [vector_space K V] {s t : set V} (ht : t.finite) :
linear_independent K (λ (x : s), x) → s (submodule.span K t) → (∃ (h : s.finite), h.to_finset.card ht.to_finset.card)

theorem linear_map.exists_left_inverse_of_injective {K : Type u_4} {V : Type u_7} {V' : Type u_8} [field K] [add_comm_group V'] [vector_space K V] [vector_space K V'] (f : V →ₗ[K] V') :
f.ker = → (∃ (g : V' →ₗ[K] V), g.comp f = linear_map.id)

theorem submodule.exists_is_compl {K : Type u_4} {V : Type u_7} [field K] [vector_space K V] (p : submodule K V) :
∃ (q : submodule K V), is_compl p q

theorem linear_map.exists_right_inverse_of_surjective {K : Type u_4} {V : Type u_7} {V' : Type u_8} [field K] [add_comm_group V'] [vector_space K V] [vector_space K V'] (f : V →ₗ[K] V') :
f.range = → (∃ (g : V' →ₗ[K] V), f.comp g = linear_map.id)

theorem quotient_prod_linear_equiv {K : Type u_4} {V : Type u_7} [field K] [vector_space K V] (p : submodule K V) :

theorem vector_space.card_fintype {K : Type u_4} {V : Type u_7} [field K] [vector_space K V] [fintype K] [fintype V] :
∃ (n : ), fintype.card V = fintype.card K ^ n

theorem pi.linear_independent_std_basis {R : Type u_3} {η : Type u_9} {ιs : η → Type u_10} {Ms : η → Type u_11} [ring R] [Π (i : η), add_comm_group (Ms i)] [Π (i : η), module R (Ms i)] (v : Π (j : η), ιs j → Ms j) :
(∀ (i : η), linear_independent R (v i)) → linear_independent R (λ (ji : Σ (j : η), ιs j), (linear_map.std_basis R Ms ji.fst) (v ji.fst ji.snd))

theorem pi.is_basis_std_basis {R : Type u_3} {η : Type u_9} {ιs : η → Type u_10} {Ms : η → Type u_11} [ring R] [Π (i : η), add_comm_group (Ms i)] [Π (i : η), module R (Ms i)] [fintype η] (s : Π (j : η), ιs j → Ms j) :
(∀ (j : η), is_basis R (s j)) → is_basis R (λ (ji : Σ (j : η), ιs j), (linear_map.std_basis R Ms ji.fst) (s ji.fst ji.snd))

theorem pi.is_basis_fun₀ (R : Type u_3) (η : Type u_9) [ring R] [fintype η] :
is_basis R (λ (ji : Σ (j : η), unit), (linear_map.std_basis R (λ (i : η), R) ji.fst) 1)

theorem pi.is_basis_fun (R : Type u_3) (η : Type u_9) [ring R] [fintype η] :
is_basis R (λ (i : η), (linear_map.std_basis R (λ (i : η), R) i) 1)