mathlib documentation

linear_algebra.basis

Bases #

This file defines 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.

Main statements #

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 ι.

Tags #

basis, bases

structure basis (ι : Type u_1) (R : Type u_3) (M : Type u_5) [semiring R] [add_comm_monoid M] [module R M] :
Type (max u_1 u_3 u_5)

A basis ι R M for a module M is the type of ι-indexed R-bases of M.

The basis vectors are available as coe_fn (b : basis ι R M) : ι → M. To turn a linear independent family of vectors spanning M into a basis, use basis.mk. They are internally represented as linear equivs M ≃ₗ[R] (ι →₀ R), available as basis.repr.

@[instance]
def basis.inhabited {ι : Type u_1} {R : Type u_3} [semiring R] :
inhabited (basis ι R →₀ R))
Equations
@[instance]
def basis.has_coe_to_fun {ι : Type u_1} {R : Type u_3} {M : Type u_5} [semiring R] [add_comm_monoid M] [module R M] :

b i is the ith basis vector.

Equations
@[simp]
theorem basis.coe_of_repr {ι : Type u_1} {R : Type u_3} {M : Type u_5} [semiring R] [add_comm_monoid M] [module R M] (e : M ≃ₗ[R] ι →₀ R) :
{repr := e} = λ (i : ι), (e.symm) (finsupp.single i 1)
theorem basis.injective {ι : Type u_1} {R : Type u_3} {M : Type u_5} [semiring R] [add_comm_monoid M] [module R M] (b : basis ι R M) [nontrivial R] :
theorem basis.repr_symm_single_one {ι : Type u_1} {R : Type u_3} {M : Type u_5} [semiring R] [add_comm_monoid M] [module R M] (b : basis ι R M) (i : ι) :
theorem basis.repr_symm_single {ι : Type u_1} {R : Type u_3} {M : Type u_5} [semiring R] [add_comm_monoid M] [module R M] (b : basis ι R M) (i : ι) (c : R) :
@[simp]
theorem basis.repr_self {ι : Type u_1} {R : Type u_3} {M : Type u_5} [semiring R] [add_comm_monoid M] [module R M] (b : basis ι R M) (i : ι) :
theorem basis.repr_self_apply {ι : Type u_1} {R : Type u_3} {M : Type u_5} [semiring R] [add_comm_monoid M] [module R M] (b : basis ι R M) (i j : ι) [decidable (i = j)] :
((b.repr) (b i)) j = ite (i = j) 1 0
@[simp]
theorem basis.repr_symm_apply {ι : Type u_1} {R : Type u_3} {M : Type u_5} [semiring R] [add_comm_monoid M] [module R M] (b : basis ι R M) (v : ι →₀ R) :
(b.repr.symm) v = (finsupp.total ι M R b) v
@[simp]
theorem basis.coe_repr_symm {ι : Type u_1} {R : Type u_3} {M : Type u_5} [semiring R] [add_comm_monoid M] [module R M] (b : basis ι R M) :
@[simp]
theorem basis.repr_total {ι : Type u_1} {R : Type u_3} {M : Type u_5} [semiring R] [add_comm_monoid M] [module R M] (b : basis ι R M) (v : ι →₀ R) :
(b.repr) ((finsupp.total ι M R b) v) = v
@[simp]
theorem basis.total_repr {ι : Type u_1} {R : Type u_3} {M : Type u_5} [semiring R] [add_comm_monoid M] [module R M] (b : basis ι R M) (x : M) :
(finsupp.total ι M R b) ((b.repr) x) = x
theorem basis.repr_range {ι : Type u_1} {R : Type u_3} {M : Type u_5} [semiring R] [add_comm_monoid M] [module R M] (b : basis ι R M) :
@[simp]
theorem basis.coord_apply {ι : Type u_1} {R : Type u_3} {M : Type u_5} [semiring R] [add_comm_monoid M] [module R M] (b : basis ι R M) (i : ι) (ᾰ : M) :
(b.coord i) = ((b.repr) ᾰ) i
def basis.coord {ι : Type u_1} {R : Type u_3} {M : Type u_5} [semiring R] [add_comm_monoid M] [module R M] (b : basis ι R M) (i : ι) :

b.coord i is the linear function giving the i'th coordinate of a vector with respect to the basis b.

b.coord i is an element of the dual space. In particular, for finite-dimensional spaces it is the ιth basis vector of the dual space.

Equations
theorem basis.forall_coord_eq_zero_iff {ι : Type u_1} {R : Type u_3} {M : Type u_5} [semiring R] [add_comm_monoid M] [module R M] (b : basis ι R M) {x : M} :
(∀ (i : ι), (b.coord i) x = 0) x = 0
theorem basis.ext {ι : Type u_1} {R : Type u_3} {M : Type u_5} [semiring R] [add_comm_monoid M] [module R M] (b : basis ι R M) {M₁ : Type u_9} [add_comm_monoid M₁] [module R M₁] {f₁ f₂ : M →ₗ[R] M₁} (h : ∀ (i : ι), f₁ (b i) = f₂ (b i)) :
f₁ = f₂

Two linear maps are equal if they are equal on basis vectors.

theorem basis.ext' {ι : Type u_1} {R : Type u_3} {M : Type u_5} [semiring R] [add_comm_monoid M] [module R M] (b : basis ι R M) {M₁ : Type u_9} [add_comm_monoid M₁] [module R M₁] {f₁ f₂ : M ≃ₗ[R] M₁} (h : ∀ (i : ι), f₁ (b i) = f₂ (b i)) :
f₁ = f₂

Two linear equivs are equal if they are equal on basis vectors.

theorem basis.ext_elem {ι : Type u_1} {R : Type u_3} {M : Type u_5} [semiring R] [add_comm_monoid M] [module R M] (b : basis ι R M) {x y : M} (h : ∀ (i : ι), ((b.repr) x) i = ((b.repr) y) i) :
x = y

Two elements are equal if their coordinates are equal.

theorem basis.repr_eq_iff {ι : Type u_1} {R : Type u_3} {M : Type u_5} [semiring R] [add_comm_monoid M] [module R M] {b : basis ι R M} {f : M →ₗ[R] ι →₀ R} :
(b.repr) = f ∀ (i : ι), f (b i) = finsupp.single i 1
theorem basis.repr_eq_iff' {ι : Type u_1} {R : Type u_3} {M : Type u_5} [semiring R] [add_comm_monoid M] [module R M] {b : basis ι R M} {f : M ≃ₗ[R] ι →₀ R} :
b.repr = f ∀ (i : ι), f (b i) = finsupp.single i 1
theorem basis.apply_eq_iff {ι : Type u_1} {R : Type u_3} {M : Type u_5} [semiring R] [add_comm_monoid M] [module R M] {b : basis ι R M} {x : M} {i : ι} :
b i = x (b.repr) x = finsupp.single i 1
theorem basis.repr_apply_eq {ι : Type u_1} {R : Type u_3} {M : Type u_5} [semiring R] [add_comm_monoid M] [module R M] (b : basis ι R M) (f : M → ι → R) (hadd : ∀ (x y : M), f (x + y) = f x + f y) (hsmul : ∀ (c : R) (x : M), f (c x) = c f x) (f_eq : ∀ (i : ι), f (b i) = (finsupp.single i 1)) (x : M) (i : ι) :
((b.repr) x) i = f x i

An unbundled version of repr_eq_iff

theorem basis.eq_of_repr_eq_repr {ι : Type u_1} {R : Type u_3} {M : Type u_5} [semiring R] [add_comm_monoid M] [module R M] {b₁ b₂ : basis ι R M} (h : ∀ (x : M) (i : ι), ((b₁.repr) x) i = ((b₂.repr) x) i) :
b₁ = b₂

Two bases are equal if they assign the same coordinates.

@[ext]
theorem basis.eq_of_apply_eq {ι : Type u_1} {R : Type u_3} {M : Type u_5} [semiring R] [add_comm_monoid M] [module R M] {b₁ b₂ : basis ι R M} (h : ∀ (i : ι), b₁ i = b₂ i) :
b₁ = b₂

Two bases are equal if their basis vectors are the same.

def basis.map {ι : Type u_1} {R : Type u_3} {M : Type u_5} {M' : Type u_6} [semiring R] [add_comm_monoid M] [module R M] [add_comm_monoid M'] [module R M'] (b : basis ι R M) (f : M ≃ₗ[R] M') :
basis ι R M'

Apply the linear equivalence f to the basis vectors.

Equations
@[simp]
theorem basis.map_repr {ι : Type u_1} {R : Type u_3} {M : Type u_5} {M' : Type u_6} [semiring R] [add_comm_monoid M] [module R M] [add_comm_monoid M'] [module R M'] (b : basis ι R M) (f : M ≃ₗ[R] M') :
(b.map f).repr = f.symm.trans b.repr
@[simp]
theorem basis.map_apply {ι : Type u_1} {R : Type u_3} {M : Type u_5} {M' : Type u_6} [semiring R] [add_comm_monoid M] [module R M] [add_comm_monoid M'] [module R M'] (b : basis ι R M) (f : M ≃ₗ[R] M') (i : ι) :
(b.map f) i = f (b i)
def basis.reindex {ι : Type u_1} {ι' : Type u_2} {R : Type u_3} {M : Type u_5} [semiring R] [add_comm_monoid M] [module R M] (b : basis ι R M) (e : ι ι') :
basis ι' R M

b.reindex (e : ι ≃ ι') is a basis indexed by ι'

Equations
theorem basis.reindex_apply {ι : Type u_1} {ι' : Type u_2} {R : Type u_3} {M : Type u_5} [semiring R] [add_comm_monoid M] [module R M] (b : basis ι R M) (e : ι ι') (i' : ι') :
(b.reindex e) i' = b ((e.symm) i')
@[simp]
theorem basis.coe_reindex {ι : Type u_1} {ι' : Type u_2} {R : Type u_3} {M : Type u_5} [semiring R] [add_comm_monoid M] [module R M] (b : basis ι R M) (e : ι ι') :
@[simp]
theorem basis.coe_reindex_repr {ι : Type u_1} {ι' : Type u_2} {R : Type u_3} {M : Type u_5} [semiring R] [add_comm_monoid M] [module R M] (b : basis ι R M) (x : M) (e : ι ι') :
(((b.reindex e).repr) x) = ((b.repr) x) (e.symm)
@[simp]
theorem basis.reindex_repr {ι : Type u_1} {ι' : Type u_2} {R : Type u_3} {M : Type u_5} [semiring R] [add_comm_monoid M] [module R M] (b : basis ι R M) (x : M) (e : ι ι') (i' : ι') :
(((b.reindex e).repr) x) i' = ((b.repr) x) ((e.symm) i')
@[simp]
theorem basis.range_reindex' {ι : Type u_1} {ι' : Type u_2} {R : Type u_3} {M : Type u_5} [semiring R] [add_comm_monoid M] [module R M] (b : basis ι R M) (e : ι ι') :

simp normal form version of range_reindex

theorem basis.range_reindex {ι : Type u_1} {ι' : Type u_2} {R : Type u_3} {M : Type u_5} [semiring R] [add_comm_monoid M] [module R M] (b : basis ι R M) (e : ι ι') :
def basis.reindex_range {ι : Type u_1} {R : Type u_3} {M : Type u_5} [semiring R] [add_comm_monoid M] [module R M] (b : basis ι R M) :

b.reindex_range is a basis indexed by range b, the basis vectors themselves.

Equations
theorem basis.finsupp.single_apply_left {α : Type u_1} {β : Type u_2} {γ : Type u_3} [has_zero γ] {f : α → β} (hf : function.injective f) (x z : α) (y : γ) :
(finsupp.single (f x) y) (f z) = (finsupp.single x y) z
theorem basis.reindex_range_self {ι : Type u_1} {R : Type u_3} {M : Type u_5} [semiring R] [add_comm_monoid M] [module R M] (b : basis ι R M) (i : ι) (h : b i set.range (λ (i : ι), b i) := _) :
(b.reindex_range) b i, h⟩ = b i
theorem basis.reindex_range_repr_self {ι : Type u_1} {R : Type u_3} {M : Type u_5} [semiring R] [add_comm_monoid M] [module R M] (b : basis ι R M) (i : ι) :
@[simp]
theorem basis.reindex_range_apply {ι : Type u_1} {R : Type u_3} {M : Type u_5} [semiring R] [add_comm_monoid M] [module R M] (b : basis ι R M) (x : (set.range b)) :
theorem basis.reindex_range_repr' {ι : Type u_1} {R : Type u_3} {M : Type u_5} [semiring R] [add_comm_monoid M] [module R M] (b : basis ι R M) (x : M) {bi : M} {i : ι} (h : b i = bi) :
((b.reindex_range.repr) x) bi, _⟩ = ((b.repr) x) i
@[simp]
theorem basis.reindex_range_repr {ι : Type u_1} {R : Type u_3} {M : Type u_5} [semiring R] [add_comm_monoid M] [module R M] (b : basis ι R M) (x : M) (i : ι) (h : b i set.range (λ (i : ι), b i) := _) :
((b.reindex_range.repr) x) b i, h⟩ = ((b.repr) x) i
def basis.reindex_finset_range {ι : Type u_1} {R : Type u_3} {M : Type u_5} [semiring R] [add_comm_monoid M] [module R M] (b : basis ι R M) [fintype ι] :

b.reindex_finset_range is a basis indexed by finset.univ.image b, the finite set of basis vectors themselves.

Equations
theorem basis.reindex_finset_range_self {ι : Type u_1} {R : Type u_3} {M : Type u_5} [semiring R] [add_comm_monoid M] [module R M] (b : basis ι R M) [fintype ι] (i : ι) (h : b i finset.image b finset.univ := _) :
@[simp]
theorem basis.reindex_finset_range_apply {ι : Type u_1} {R : Type u_3} {M : Type u_5} [semiring R] [add_comm_monoid M] [module R M] (b : basis ι R M) [fintype ι] (x : (finset.image b finset.univ)) :
theorem basis.reindex_finset_range_repr_self {ι : Type u_1} {R : Type u_3} {M : Type u_5} [semiring R] [add_comm_monoid M] [module R M] (b : basis ι R M) [fintype ι] (i : ι) :
@[simp]
theorem basis.reindex_finset_range_repr {ι : Type u_1} {R : Type u_3} {M : Type u_5} [semiring R] [add_comm_monoid M] [module R M] (b : basis ι R M) [fintype ι] (x : M) (i : ι) (h : b i finset.image b finset.univ := _) :
theorem basis.linear_independent {ι : Type u_1} {R : Type u_3} {M : Type u_5} [semiring R] [add_comm_monoid M] [module R M] (b : basis ι R M) :
theorem basis.ne_zero {ι : Type u_1} {R : Type u_3} {M : Type u_5} [semiring R] [add_comm_monoid M] [module R M] (b : basis ι R M) [nontrivial R] (i : ι) :
b i 0
theorem basis.mem_span {ι : Type u_1} {R : Type u_3} {M : Type u_5} [semiring R] [add_comm_monoid M] [module R M] (b : basis ι R M) (x : M) :
theorem basis.span_eq {ι : Type u_1} {R : Type u_3} {M : Type u_5} [semiring R] [add_comm_monoid M] [module R M] (b : basis ι R M) :
def basis.constr {ι : Type u_1} {R : Type u_3} {M : Type u_5} {M' : Type u_6} [semiring R] [add_comm_monoid M] [module R M] [add_comm_monoid M'] [module R M'] (b : basis ι R M) (S : Type u_9) [semiring S] [module S M'] [smul_comm_class R S M'] :
(ι → M') ≃ₗ[S] M →ₗ[R] M'

Construct a linear map given the value at the basis.

This definition is parameterized over an extra semiring S, such that smul_comm_class R S M' holds. If R is commutative, you can set S := R; if R is not commutative, you can recover an add_equiv by setting S := ℕ. See library note [bundled maps over different rings].

Equations
theorem basis.constr_def {ι : Type u_1} {R : Type u_3} {M : Type u_5} {M' : Type u_6} [semiring R] [add_comm_monoid M] [module R M] [add_comm_monoid M'] [module R M'] (b : basis ι R M) (S : Type u_9) [semiring S] [module S M'] [smul_comm_class R S M'] (f : ι → M') :
theorem basis.constr_apply {ι : Type u_1} {R : Type u_3} {M : Type u_5} {M' : Type u_6} [semiring R] [add_comm_monoid M] [module R M] [add_comm_monoid M'] [module R M'] (b : basis ι R M) (S : Type u_9) [semiring S] [module S M'] [smul_comm_class R S M'] (f : ι → M') (x : M) :
((b.constr S) f) x = ((b.repr) x).sum (λ (b : ι) (a : R), a f b)
@[simp]
theorem basis.constr_basis {ι : Type u_1} {R : Type u_3} {M : Type u_5} {M' : Type u_6} [semiring R] [add_comm_monoid M] [module R M] [add_comm_monoid M'] [module R M'] (b : basis ι R M) (S : Type u_9) [semiring S] [module S M'] [smul_comm_class R S M'] (f : ι → M') (i : ι) :
((b.constr S) f) (b i) = f i
theorem basis.constr_eq {ι : Type u_1} {R : Type u_3} {M : Type u_5} {M' : Type u_6} [semiring R] [add_comm_monoid M] [module R M] [add_comm_monoid M'] [module R M'] (b : basis ι R M) (S : Type u_9) [semiring S] [module S M'] [smul_comm_class R S M'] {g : ι → M'} {f : M →ₗ[R] M'} (h : ∀ (i : ι), g i = f (b i)) :
(b.constr S) g = f
theorem basis.constr_self {ι : Type u_1} {R : Type u_3} {M : Type u_5} {M' : Type u_6} [semiring R] [add_comm_monoid M] [module R M] [add_comm_monoid M'] [module R M'] (b : basis ι R M) (S : Type u_9) [semiring S] [module S M'] [smul_comm_class R S M'] (f : M →ₗ[R] M') :
(b.constr S) (λ (i : ι), f (b i)) = f
theorem basis.constr_range {ι : Type u_1} {R : Type u_3} {M : Type u_5} {M' : Type u_6} [semiring R] [add_comm_monoid M] [module R M] [add_comm_monoid M'] [module R M'] (b : basis ι R M) (S : Type u_9) [semiring S] [module S M'] [smul_comm_class R S M'] [nonempty ι] {f : ι → M'} :
@[simp]
theorem basis.constr_comp {ι : Type u_1} {R : Type u_3} {M : Type u_5} {M' : Type u_6} [semiring R] [add_comm_monoid M] [module R M] [add_comm_monoid M'] [module R M'] (b : basis ι R M) (S : Type u_9) [semiring S] [module S M'] [smul_comm_class R S M'] (f : M' →ₗ[R] M') (v : ι → M') :
(b.constr S) (f v) = f.comp ((b.constr S) v)
def basis.equiv {ι : Type u_1} {ι' : Type u_2} {R : Type u_3} {M : Type u_5} {M' : Type u_6} [semiring R] [add_comm_monoid M] [module R M] [add_comm_monoid M'] [module R M'] (b : basis ι R M) (b' : basis ι' R M') (e : ι ι') :
M ≃ₗ[R] M'

If b is a basis for M and b' a basis for M', and the index types are equivalent, b.equiv b' e is a linear equivalence M ≃ₗ[R] M', mapping b i to b' (e i).

Equations
@[simp]
theorem basis.equiv_apply {ι : Type u_1} {ι' : Type u_2} {R : Type u_3} {M : Type u_5} {M' : Type u_6} [semiring R] [add_comm_monoid M] [module R M] [add_comm_monoid M'] [module R M'] (b : basis ι R M) (i : ι) (b' : basis ι' R M') (e : ι ι') :
(b.equiv b' e) (b i) = b' (e i)
@[simp]
theorem basis.equiv_refl {ι : Type u_1} {R : Type u_3} {M : Type u_5} [semiring R] [add_comm_monoid M] [module R M] (b : basis ι R M) :
@[simp]
theorem basis.equiv_symm {ι : Type u_1} {ι' : Type u_2} {R : Type u_3} {M : Type u_5} {M' : Type u_6} [semiring R] [add_comm_monoid M] [module R M] [add_comm_monoid M'] [module R M'] (b : basis ι R M) (b' : basis ι' R M') (e : ι ι') :
(b.equiv b' e).symm = b'.equiv b e.symm
@[simp]
theorem basis.equiv_trans {ι : Type u_1} {ι' : Type u_2} {R : Type u_3} {M : Type u_5} {M' : Type u_6} {M'' : Type u_7} [semiring R] [add_comm_monoid M] [module R M] [add_comm_monoid M'] [module R M'] (b : basis ι R M) (b' : basis ι' R M') [add_comm_monoid M''] [module R M''] {ι'' : Type u_4} (b'' : basis ι'' R M'') (e : ι ι') (e' : ι' ι'') :
(b.equiv b' e).trans (b'.equiv b'' e') = b.equiv b'' (e.trans e')
@[simp]
theorem basis.map_equiv {ι : Type u_1} {ι' : Type u_2} {R : Type u_3} {M : Type u_5} {M' : Type u_6} [semiring R] [add_comm_monoid M] [module R M] [add_comm_monoid M'] [module R M'] (b : basis ι R M) (b' : basis ι' R M') (e : ι ι') :
b.map (b.equiv b' e) = b'.reindex e.symm
def basis.prod {ι : Type u_1} {ι' : Type u_2} {R : Type u_3} {M : Type u_5} {M' : Type u_6} [semiring R] [add_comm_monoid M] [module R M] [add_comm_monoid M'] [module R M'] (b : basis ι R M) (b' : basis ι' R M') :
basis ι') R (M × M')

basis.prod maps a ι-indexed basis for M and a ι'-indexed basis for M' to a ι ⊕ ι'-index basis for M × M'.

Equations
@[simp]
theorem basis.prod_repr_inl {ι : Type u_1} {ι' : Type u_2} {R : Type u_3} {M : Type u_5} {M' : Type u_6} [semiring R] [add_comm_monoid M] [module R M] [add_comm_monoid M'] [module R M'] (b : basis ι R M) (b' : basis ι' R M') (x : M × M') (i : ι) :
(((b.prod b').repr) x) (sum.inl i) = ((b.repr) x.fst) i
@[simp]
theorem basis.prod_repr_inr {ι : Type u_1} {ι' : Type u_2} {R : Type u_3} {M : Type u_5} {M' : Type u_6} [semiring R] [add_comm_monoid M] [module R M] [add_comm_monoid M'] [module R M'] (b : basis ι R M) (b' : basis ι' R M') (x : M × M') (i : ι') :
(((b.prod b').repr) x) (sum.inr i) = ((b'.repr) x.snd) i
theorem basis.prod_apply_inl_fst {ι : Type u_1} {ι' : Type u_2} {R : Type u_3} {M : Type u_5} {M' : Type u_6} [semiring R] [add_comm_monoid M] [module R M] [add_comm_monoid M'] [module R M'] (b : basis ι R M) (b' : basis ι' R M') (i : ι) :
((b.prod b') (sum.inl i)).fst = b i
theorem basis.prod_apply_inr_fst {ι : Type u_1} {ι' : Type u_2} {R : Type u_3} {M : Type u_5} {M' : Type u_6} [semiring R] [add_comm_monoid M] [module R M] [add_comm_monoid M'] [module R M'] (b : basis ι R M) (b' : basis ι' R M') (i : ι') :
((b.prod b') (sum.inr i)).fst = 0
theorem basis.prod_apply_inl_snd {ι : Type u_1} {ι' : Type u_2} {R : Type u_3} {M : Type u_5} {M' : Type u_6} [semiring R] [add_comm_monoid M] [module R M] [add_comm_monoid M'] [module R M'] (b : basis ι R M) (b' : basis ι' R M') (i : ι) :
((b.prod b') (sum.inl i)).snd = 0
theorem basis.prod_apply_inr_snd {ι : Type u_1} {ι' : Type u_2} {R : Type u_3} {M : Type u_5} {M' : Type u_6} [semiring R] [add_comm_monoid M] [module R M] [add_comm_monoid M'] [module R M'] (b : basis ι R M) (b' : basis ι' R M') (i : ι') :
((b.prod b') (sum.inr i)).snd = b' i
@[simp]
theorem basis.prod_apply {ι : Type u_1} {ι' : Type u_2} {R : Type u_3} {M : Type u_5} {M' : Type u_6} [semiring R] [add_comm_monoid M] [module R M] [add_comm_monoid M'] [module R M'] (b : basis ι R M) (b' : basis ι' R M') (i : ι ι') :
(b.prod b') i = sum.elim ((linear_map.inl R M M') b) ((linear_map.inr R M M') b') i
theorem basis.no_zero_smul_divisors {ι : Type u_1} {R : Type u_3} {M : Type u_5} [semiring R] [add_comm_monoid M] [module R M] [no_zero_divisors R] (b : basis ι R M) :
theorem basis.smul_eq_zero {ι : Type u_1} {R : Type u_3} {M : Type u_5} [semiring R] [add_comm_monoid M] [module R M] [no_zero_divisors R] (b : basis ι R M) {c : R} {x : M} :
c x = 0 c = 0 x = 0
def basis.singleton (ι : Type u_1) (R : Type u_2) [unique ι] [semiring R] :
basis ι R R

basis.singleton ι R is the basis sending the unique element of ι to 1 : R.

Equations
@[simp]
theorem basis.singleton_apply (ι : Type u_1) (R : Type u_2) [unique ι] [semiring R] (i : ι) :
@[simp]
theorem basis.singleton_repr (ι : Type u_1) (R : Type u_2) [unique ι] [semiring R] (x : R) (i : ι) :
(((basis.singleton ι R).repr) x) i = x
theorem basis.basis_singleton_iff {R : Type u_1} {M : Type u_2} [ring R] [nontrivial R] [add_comm_group M] [module R M] [no_zero_smul_divisors R M] (ι : Type u_3) [unique ι] :
nonempty (basis ι R M) ∃ (x : M) (H : x 0), ∀ (y : M), ∃ (r : R), r x = y
def basis.empty {ι : Type u_1} {R : Type u_3} (M : Type u_5) [semiring R] [add_comm_monoid M] [module R M] [subsingleton M] [is_empty ι] :
basis ι R M

If M is a subsingleton and ι is empty, this is the unique ι-indexed basis for M.

Equations
@[instance]
def basis.empty_unique {ι : Type u_1} {R : Type u_3} (M : Type u_5) [semiring R] [add_comm_monoid M] [module R M] [subsingleton M] [is_empty ι] :
unique (basis ι R M)
Equations
def basis.equiv_fun {ι : Type u_1} {R : Type u_3} {M : Type u_5} [semiring R] [add_comm_monoid M] [module R M] [fintype ι] (b : basis ι R M) :
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} [semiring R] [add_comm_monoid M] [module R M] [fintype ι] (b : basis ι R M) [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} [semiring R] [add_comm_monoid M] [module R M] [fintype ι] (b : basis ι R M) [fintype R] [fintype M] :
@[simp]
theorem basis.equiv_fun_symm_apply {ι : Type u_1} {R : Type u_3} {M : Type u_5} [semiring R] [add_comm_monoid M] [module R M] [fintype ι] (b : basis ι R M) (x : ι → R) :
(b.equiv_fun.symm) x = ∑ (i : ι), x i b 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.

@[simp]
theorem basis.equiv_fun_apply {ι : Type u_1} {R : Type u_3} {M : Type u_5} [semiring R] [add_comm_monoid M] [module R M] [fintype ι] (b : basis ι R M) (u : M) :
(b.equiv_fun) u = ((b.repr) u)
theorem basis.sum_equiv_fun {ι : Type u_1} {R : Type u_3} {M : Type u_5} [semiring R] [add_comm_monoid M] [module R M] [fintype ι] (b : basis ι R M) (u : M) :
∑ (i : ι), (b.equiv_fun) u i b i = u
theorem basis.sum_repr {ι : Type u_1} {R : Type u_3} {M : Type u_5} [semiring R] [add_comm_monoid M] [module R M] [fintype ι] (b : basis ι R M) (u : M) :
∑ (i : ι), ((b.repr) u) i b i = u
@[simp]
theorem basis.equiv_fun_self {ι : Type u_1} {R : Type u_3} {M : Type u_5} [semiring R] [add_comm_monoid M] [module R M] [fintype ι] (b : basis ι R M) (i j : ι) :
(b.equiv_fun) (b i) j = ite (i = j) 1 0
def basis.of_equiv_fun {ι : Type u_1} {R : Type u_3} {M : Type u_5} [semiring R] [add_comm_monoid M] [module R M] [fintype ι] (e : M ≃ₗ[R] ι → R) :
basis ι R M

Define a basis by mapping each vector x : M to its coordinates e x : ι → R, as long as ι is finite.

Equations
@[simp]
theorem basis.of_equiv_fun_repr_apply {ι : Type u_1} {R : Type u_3} {M : Type u_5} [semiring R] [add_comm_monoid M] [module R M] [fintype ι] (e : M ≃ₗ[R] ι → R) (x : M) (i : ι) :
@[simp]
theorem basis.coe_of_equiv_fun {ι : Type u_1} {R : Type u_3} {M : Type u_5} [semiring R] [add_comm_monoid M] [module R M] [fintype ι] (e : M ≃ₗ[R] ι → R) :
(basis.of_equiv_fun e) = λ (i : ι), (e.symm) (function.update 0 i 1)
@[simp]
theorem basis.constr_apply_fintype {ι : Type u_1} {R : Type u_3} {M : Type u_5} {M' : Type u_6} [semiring R] [add_comm_monoid M] [module R M] [add_comm_monoid M'] [module R M'] [fintype ι] (b : basis ι R M) (S : Type u_9) [semiring S] [module S M'] [smul_comm_class R S M'] (f : ι → M') (x : M) :
((b.constr S) f) x = ∑ (i : ι), (b.equiv_fun) x i f i
def basis.equiv' {ι : Type u_1} {ι' : Type u_2} {R : Type u_3} {M : Type u_5} {M' : Type u_6} [comm_semiring R] [add_comm_monoid M] [module R M] [add_comm_monoid M'] [module R M'] (b : basis ι R M) (b' : basis ι' R M') (f : M → M') (g : M' → M) (hf : ∀ (i : ι), f (b i) set.range b') (hg : ∀ (i : ι'), g (b' i) set.range b) (hgf : ∀ (i : ι), g (f (b i)) = b i) (hfg : ∀ (i : ι'), f (g (b' i)) = b' i) :
M ≃ₗ[R] M'

If b is a basis for M and b' a basis for M', and f, g form a bijection between the basis vectors, b.equiv' b' f g hf hg hgf hfg is a linear equivalence M ≃ₗ[R] M', mapping b i to f (b i).

Equations
@[simp]
theorem basis.equiv'_apply {ι : Type u_1} {ι' : Type u_2} {R : Type u_3} {M : Type u_5} {M' : Type u_6} [comm_semiring R] [add_comm_monoid M] [module R M] [add_comm_monoid M'] [module R M'] (b : basis ι R M) (b' : basis ι' R M') (f : M → M') (g : M' → M) (hf : ∀ (i : ι), f (b i) set.range b') (hg : ∀ (i : ι'), g (b' i) set.range b) (hgf : ∀ (i : ι), g (f (b i)) = b i) (hfg : ∀ (i : ι'), f (g (b' i)) = b' i) (i : ι) :
(b.equiv' b' f g hf hg hgf hfg) (b i) = f (b i)
@[simp]
theorem basis.equiv'_symm_apply {ι : Type u_1} {ι' : Type u_2} {R : Type u_3} {M : Type u_5} {M' : Type u_6} [comm_semiring R] [add_comm_monoid M] [module R M] [add_comm_monoid M'] [module R M'] (b : basis ι R M) (b' : basis ι' R M') (f : M → M') (g : M' → M) (hf : ∀ (i : ι), f (b i) set.range b') (hg : ∀ (i : ι'), g (b' i) set.range b) (hgf : ∀ (i : ι), g (f (b i)) = b i) (hfg : ∀ (i : ι'), f (g (b' i)) = b' i) (i : ι') :
((b.equiv' b' f g hf hg hgf hfg).symm) (b' i) = g (b' i)
theorem basis.sum_repr_mul_repr {ι : Type u_1} {R : Type u_3} {M : Type u_5} [comm_semiring R] [add_comm_monoid M] [module R M] (b : basis ι R M) {ι' : Type u_2} [fintype ι'] (b' : basis ι' R M) (x : M) (i : ι) :
∑ (j : ι'), (((b.repr) (b' j)) i) * ((b'.repr) x) j = ((b.repr) x) i
def basis.mk {ι : Type u_1} {R : Type u_3} {M : Type u_5} {v : ι → M} [ring R] [add_comm_group M] [module R M] (hli : linear_independent R v) (hsp : submodule.span R (set.range v) = ) :
basis ι R M

A linear independent family of vectors spanning the whole module is a basis.

Equations
@[simp]
theorem basis.mk_repr {ι : Type u_1} {R : Type u_3} {M : Type u_5} {v : ι → M} [ring R] [add_comm_group M] [module R M] {x : M} (hli : linear_independent R v) (hsp : submodule.span R (set.range v) = ) :
((basis.mk hli hsp).repr) x = (hli.repr) x, _⟩
theorem basis.mk_apply {ι : Type u_1} {R : Type u_3} {M : Type u_5} {v : ι → M} [ring R] [add_comm_group M] [module R M] (hli : linear_independent R v) (hsp : submodule.span R (set.range v) = ) (i : ι) :
(basis.mk hli hsp) i = v i
@[simp]
theorem basis.coe_mk {ι : Type u_1} {R : Type u_3} {M : Type u_5} {v : ι → M} [ring R] [add_comm_group M] [module R M] (hli : linear_independent R v) (hsp : submodule.span R (set.range v) = ) :
(basis.mk hli hsp) = v
def basis.span {ι : Type u_1} {R : Type u_3} {M : Type u_5} {v : ι → M} [ring R] [add_comm_group M] [module R M] (hli : linear_independent R v) :

A linear independent family of vectors is a basis for their span.

Equations
theorem basis.group_smul_span_eq_top {ι : Type u_1} {R : Type u_3} {M : Type u_5} [ring R] [add_comm_group M] [module R M] {G : Type u_2} [group G] [distrib_mul_action G R] [distrib_mul_action G M] [is_scalar_tower G R M] {v : ι → M} (hv : submodule.span R (set.range v) = ) {w : ι → G} :
def basis.group_smul {ι : Type u_1} {R : Type u_3} {M : Type u_5} [ring R] [add_comm_group M] [module R M] {G : Type u_2} [group G] [distrib_mul_action G R] [distrib_mul_action G M] [is_scalar_tower G R M] [smul_comm_class G R M] (v : basis ι R M) (w : ι → G) :
basis ι R M

Given a basis v and a map w such that for all i, w i are elements of a group, group_smul provides the basis corresponding to w • v.

Equations
theorem basis.group_smul_apply {ι : Type u_1} {R : Type u_3} {M : Type u_5} [ring R] [add_comm_group M] [module R M] {G : Type u_2} [group G] [distrib_mul_action G R] [distrib_mul_action G M] [is_scalar_tower G R M] [smul_comm_class G R M] {v : basis ι R M} {w : ι → G} (i : ι) :
(v.group_smul w) i = (w v) i
theorem basis.units_smul_span_eq_top {ι : Type u_1} {R : Type u_3} {M : Type u_5} [ring R] [add_comm_group M] [module R M] {v : ι → M} (hv : submodule.span R (set.range v) = ) {w : ι → units R} :
def basis.units_smul {ι : Type u_1} {R : Type u_3} {M : Type u_5} [ring R] [add_comm_group M] [module R M] (v : basis ι R M) (w : ι → units R) :
basis ι R M

Given a basis v and a map w such that for all i, w i is a unit, smul_of_is_unit provides the basis corresponding to w • v.

Equations
theorem basis.units_smul_apply {ι : Type u_1} {R : Type u_3} {M : Type u_5} [ring R] [add_comm_group M] [module R M] {v : basis ι R M} {w : ι → units R} (i : ι) :
(v.units_smul w) i = w i v i
def basis.is_unit_smul {ι : Type u_1} {R : Type u_3} {M : Type u_5} [ring R] [add_comm_group M] [module R M] (v : basis ι R M) {w : ι → R} (hw : ∀ (i : ι), is_unit (w i)) :
basis ι R M

A version of smul_of_units that uses is_unit.

Equations
theorem basis.is_unit_smul_apply {ι : Type u_1} {R : Type u_3} {M : Type u_5} [ring R] [add_comm_group M] [module R M] {v : basis ι R M} {w : ι → R} (hw : ∀ (i : ι), is_unit (w i)) (i : ι) :
(v.is_unit_smul hw) i = w i v i
def basis.extend {K : Type u_4} {V : Type u} [division_ring K] [add_comm_group V] [module K V] {s : set V} (hs : linear_independent K coe) :
basis (hs.extend _) K V

If s is a linear independent set of vectors, we can extend it to a basis.

Equations
theorem basis.extend_apply_self {K : Type u_4} {V : Type u} [division_ring K] [add_comm_group V] [module K V] {s : set V} (hs : linear_independent K coe) (x : (hs.extend _)) :
@[simp]
theorem basis.coe_extend {K : Type u_4} {V : Type u} [division_ring K] [add_comm_group V] [module K V] {s : set V} (hs : linear_independent K coe) :
theorem basis.range_extend {K : Type u_4} {V : Type u} [division_ring K] [add_comm_group V] [module K V] {s : set V} (hs : linear_independent K coe) :
def basis.sum_extend {ι : Type u_1} {K : Type u_4} {V : Type u} [division_ring K] [add_comm_group V] [module K V] {v : ι → V} (hs : linear_independent K v) :
basis (_.extend basis.sum_extend._proof_2 \ set.range v)) K V

If v is a linear independent family of vectors, extend it to a basis indexed by a sum type.

Equations
theorem basis.subset_extend {K : Type u_4} {V : Type u} [division_ring K] [add_comm_group V] [module K V] {s : set V} (hs : linear_independent K coe) :
s hs.extend _
def basis.of_vector_space_index (K : Type u_4) (V : Type u) [division_ring K] [add_comm_group V] [module K V] :
set V

A set used to index basis.of_vector_space.

Equations
def basis.of_vector_space (K : Type u_4) (V : Type u) [division_ring K] [add_comm_group V] [module K V] :

Each vector space has a basis.

Equations
@[simp]
theorem basis.coe_of_vector_space (K : Type u_4) (V : Type u) [division_ring K] [add_comm_group V] [module K V] :
theorem basis.exists_basis (K : Type u_4) (V : Type u) [division_ring K] [add_comm_group V] [module K V] :
∃ (s : set V), nonempty (basis s K V)
theorem vector_space.card_fintype (K : Type u_4) (V : Type u) [division_ring K] [add_comm_group V] [module K V] [fintype K] [fintype V] :
∃ (n : ), fintype.card V = fintype.card K ^ n
theorem linear_map.exists_left_inverse_of_injective {K : Type u_4} {V : Type u} {V' : Type u_8} [field K] [add_comm_group V] [add_comm_group V'] [module K V] [module K V'] (f : V →ₗ[K] V') (hf_inj : f.ker = ) :
∃ (g : V' →ₗ[K] V), g.comp f = linear_map.id
theorem submodule.exists_is_compl {K : Type u_4} {V : Type u} [field K] [add_comm_group V] [module K V] (p : submodule K V) :
∃ (q : submodule K V), is_compl p q
@[instance]
def module.submodule.is_complemented {K : Type u_4} {V : Type u} [field K] [add_comm_group V] [module K V] :
theorem linear_map.exists_right_inverse_of_surjective {K : Type u_4} {V : Type u} {V' : Type u_8} [field K] [add_comm_group V] [add_comm_group V'] [module K V] [module K V'] (f : V →ₗ[K] V') (hf_surj : f.range = ) :
∃ (g : V' →ₗ[K] V), f.comp g = linear_map.id
theorem linear_map.exists_extend {K : Type u_4} {V : Type u} {V' : Type u_8} [field K] [add_comm_group V] [add_comm_group V'] [module K V] [module K V'] {p : submodule K V} (f : p →ₗ[K] V') :
∃ (g : V →ₗ[K] V'), g.comp p.subtype = f

Any linear map f : p →ₗ[K] V' defined on a subspace p can be extended to the whole space.

theorem submodule.exists_le_ker_of_lt_top {K : Type u_4} {V : Type u} [field K] [add_comm_group V] [module K V] (p : submodule K V) (hp : p < ) :
∃ (f : V →ₗ[K] K) (H : f 0), p f.ker

If p < ⊤ is a subspace of a vector space V, then there exists a nonzero linear map f : V →ₗ[K] K such that p ≤ ker f.

theorem quotient_prod_linear_equiv {K : Type u_4} {V : Type u} [field K] [add_comm_group V] [module K V] (p : submodule K V) :