Lean mathlib docs

linear_algebra.basis

constr_add
constr_basis
constr_eq
constr_neg
constr_range
constr_self
constr_smul
constr_sub
constr_zero
disjoint_span_singleton
eq_of_linear_independent_of_span_subtype
equiv_fun_basis
equiv_fun_basis_symm_apply
equiv_of_is_basis
equiv_of_is_basis'
exists_finite_card_le_of_finite_of_linear_independent_of_span
exists_is_basis
exists_linear_independent
exists_of_linear_independent_of_finite_span
exists_subset_is_basis
is_basis
is_basis.comp
is_basis.constr
is_basis.constr_apply
is_basis.ext
is_basis.injective
is_basis.mem_span
is_basis.repr
is_basis.repr_eq_single
is_basis.repr_ker
is_basis.repr_range
is_basis.repr_total
is_basis.total_comp_repr
is_basis.total_repr
is_basis_empty
is_basis_empty_bot
is_basis_inl_union_inr
is_basis_singleton_one
is_basis_span
le_of_span_le_span
linear_equiv.is_basis
linear_independent
linear_independent.comp
linear_independent.image
linear_independent.image_subtype
linear_independent.injective
linear_independent.inl_union_inr
linear_independent.insert
linear_independent.mono
linear_independent.ne_zero
linear_independent.of_subtype_range
linear_independent.repr
linear_independent.repr_eq
linear_independent.repr_eq_single
linear_independent.repr_ker
linear_independent.repr_range
linear_independent.restrict_of_comp_subtype
linear_independent.to_subtype_range
linear_independent.total_comp_repr
linear_independent.total_equiv
linear_independent.total_repr
linear_independent.union
linear_independent.unique
linear_independent_Union_finite
linear_independent_Union_finite_subtype
linear_independent_Union_of_directed
linear_independent_bUnion_of_directed
linear_independent_comp_subtype
linear_independent_comp_subtype_disjoint
linear_independent_empty
linear_independent_empty_type
linear_independent_iff
linear_independent_iff'
linear_independent_iff_not_mem_span
linear_independent_iff_not_smul_mem_span
linear_independent_iff_total_on
linear_independent_inl_union_inr'
linear_independent_monoid_hom
linear_independent_of_finite
linear_independent_of_zero_eq_one
linear_independent_sUnion_of_directed
linear_independent_singleton
linear_independent_span
linear_independent_subtype
linear_independent_subtype_disjoint
linear_independent_unique
linear_map.exists_left_inverse_of_injective
linear_map.exists_right_inverse_of_surjective
mem_span_insert_exchange
module.card_fintype
module.fintype_of_fintype
module_equiv_finsupp
pi.is_basis_fun
pi.is_basis_fun₀
pi.is_basis_std_basis
pi.linear_independent_std_basis
quotient_prod_linear_equiv
span_le_span_iff
submodule.exists_is_compl
surjective_of_linear_independent_of_span
vector_space.card_fintype

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] [add_comm_group M] [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] [add_comm_group M] [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] [add_comm_group M] [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] [add_comm_group M] [module R M] :

theorem linear_independent.ne_zero {ι : Type u_1} {R : Type u_3} {M : Type u_5} {v : ι → M} [ring R] [add_comm_group M] [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] [add_comm_group M] [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] [add_comm_group M] [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] [add_comm_group M] [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] [add_comm_group M] [module R M] :

theorem linear_independent_span {ι : Type u_1} {R : Type u_3} {M : Type u_5} {v : ι → M} [ring R] [add_comm_group M] [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] [add_comm_group M] [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] [add_comm_group M] [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] [add_comm_group M] [module R M] {s : set ι} :

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

theorem linear_independent_iff_total_on {R : Type u_3} {M : Type u_5} [ring R] [add_comm_group M] [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] [add_comm_group M] [module R M] :

theorem linear_independent.of_subtype_range {ι : Type u_1} {R : Type u_3} {M : Type u_5} {v : ι → M} [ring R] [add_comm_group M] [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] [add_comm_group M] [module R M] {s : set ι} :

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

theorem linear_independent.mono {R : Type u_3} {M : Type u_5} [ring R] [add_comm_group M] [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] [add_comm_group M] [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] [add_comm_group M] [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] [add_comm_group M] [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] [add_comm_group M] [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] [add_comm_group M] [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] [add_comm_group M] [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] [add_comm_group M] [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] [add_comm_group M] [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] [add_comm_group M] [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] [add_comm_group M] [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] [add_comm_group M] [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] [add_comm_group M] [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] [add_comm_group M] [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] [add_comm_group M] [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] [add_comm_group M] [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] [add_comm_group M] [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] [add_comm_group M] [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] [add_comm_group M] [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] [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] [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] [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] [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) [integral_domain L] :
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] [add_comm_group M] [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] [add_comm_group M] [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] [add_comm_group M] [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] [add_comm_group M] [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] [add_comm_group M] [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] [add_comm_group M] [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] [add_comm_group M] [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] [add_comm_group M] [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] [add_comm_group M] [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] [add_comm_group M] [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] [add_comm_group M] [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] [add_comm_group M] [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] [add_comm_group M] [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] [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] [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] [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] [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] [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] [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] [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] [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] [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] [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] [add_comm_group M] [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] [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] [add_comm_group M] [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] [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] [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] [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] [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] [add_comm_group M] [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] [add_comm_group M] [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] [add_comm_group M] [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] [add_comm_group M] [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] [add_comm_group M] [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] [add_comm_group M] [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] [add_comm_group M] [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] [add_comm_group V] [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] [add_comm_group V] [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] [add_comm_group V] [vector_space K V] [unique ι] :

theorem linear_independent_singleton {K : Type u_4} {V : Type u_7} [field K] [add_comm_group V] [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] [add_comm_group V] [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] [add_comm_group V] [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] [add_comm_group V] [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] [add_comm_group V] [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] [add_comm_group V] [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] [add_comm_group V] [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] [add_comm_group V] [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] [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] [add_comm_group V] [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] [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] [add_comm_group V] [vector_space K V] (p : submodule K V) :

theorem vector_space.card_fintype {K : Type u_4} {V : Type u_7} [field K] [add_comm_group V] [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)