mathlib documentation

linear_algebra.basis

Bases #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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_6) [semiring R] [add_comm_monoid M] [module R M] :
Type (max u_1 u_3 u_6)

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.

Instances for basis
@[protected, instance]
noncomputable def unique_basis {ι : Type u_1} {R : Type u_3} {M : Type u_6} [semiring R] [add_comm_monoid M] [module R M] [subsingleton R] :
unique (basis ι R M)
Equations
@[protected, instance]
noncomputable def basis.inhabited {ι : Type u_1} {R : Type u_3} [semiring R] :
inhabited (basis ι R →₀ R))
Equations
theorem basis.repr_injective {ι : Type u_1} {R : Type u_3} {M : Type u_6} [semiring R] [add_comm_monoid M] [module R M] :
@[protected, instance]
noncomputable def basis.fun_like {ι : Type u_1} {R : Type u_3} {M : Type u_6} [semiring R] [add_comm_monoid M] [module R M] :
fun_like (basis ι R M) ι (λ (_x : ι), 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_6} [semiring R] [add_comm_monoid M] [module R M] (e : M ≃ₗ[R] ι →₀ R) :
{repr := e} = λ (i : ι), (e.symm) (finsupp.single i 1)
@[protected]
theorem basis.injective {ι : Type u_1} {R : Type u_3} {M : Type u_6} [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_6} [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_6} [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_6} [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_6} [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_6} [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_6} [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_6} [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_6} [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_6} [semiring R] [add_comm_monoid M] [module R M] (b : basis ι R M) :
theorem basis.mem_span_repr_support {R : Type u_3} {M : Type u_6} [semiring R] [add_comm_monoid M] [module R M] {ι : Type u_1} (b : basis ι R M) (m : M) :
theorem basis.repr_support_subset_of_mem_span {R : Type u_3} {M : Type u_6} [semiring R] [add_comm_monoid M] [module R M] {ι : Type u_1} (b : basis ι R M) (s : set ι) {m : M} (hm : m submodule.span R (b '' s)) :
(((b.repr) m).support) s
@[simp]
theorem basis.coord_apply {ι : Type u_1} {R : Type u_3} {M : Type u_6} [semiring R] [add_comm_monoid M] [module R M] (b : basis ι R M) (i : ι) (ᾰ : M) :
(b.coord i) = ((b.repr) ᾰ) i
noncomputable def basis.coord {ι : Type u_1} {R : Type u_3} {M : Type u_6} [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_6} [semiring R] [add_comm_monoid M] [module R M] (b : basis ι R M) {x : M} :
( (i : ι), (b.coord i) x = 0) x = 0
noncomputable def basis.sum_coords {ι : Type u_1} {R : Type u_3} {M : Type u_6} [semiring R] [add_comm_monoid M] [module R M] (b : basis ι R M) :

The sum of the coordinates of an element m : M with respect to a basis.

Equations
@[simp]
theorem basis.coe_sum_coords {ι : Type u_1} {R : Type u_3} {M : Type u_6} [semiring R] [add_comm_monoid M] [module R M] (b : basis ι R M) :
(b.sum_coords) = λ (m : M), ((b.repr) m).sum (λ (i : ι), id)
theorem basis.coe_sum_coords_eq_finsum {ι : Type u_1} {R : Type u_3} {M : Type u_6} [semiring R] [add_comm_monoid M] [module R M] (b : basis ι R M) :
(b.sum_coords) = λ (m : M), finsum (λ (i : ι), (b.coord i) m)
@[simp]
theorem basis.coe_sum_coords_of_fintype {ι : Type u_1} {R : Type u_3} {M : Type u_6} [semiring R] [add_comm_monoid M] [module R M] (b : basis ι R M) [fintype ι] :
(b.sum_coords) = finset.univ.sum (λ (i : ι), (b.coord i))
@[simp]
theorem basis.sum_coords_self_apply {ι : Type u_1} {R : Type u_3} {M : Type u_6} [semiring R] [add_comm_monoid M] [module R M] (b : basis ι R M) (i : ι) :
(b.sum_coords) (b i) = 1
theorem basis.dvd_coord_smul {ι : Type u_1} {R : Type u_3} {M : Type u_6} [semiring R] [add_comm_monoid M] [module R M] (b : basis ι R M) (i : ι) (m : M) (r : R) :
r (b.coord i) (r m)
theorem basis.coord_repr_symm {ι : Type u_1} {R : Type u_3} {M : Type u_6} [semiring R] [add_comm_monoid M] [module R M] (b : basis ι R M) (i : ι) (f : ι →₀ R) :
(b.coord i) ((b.repr.symm) f) = f i
theorem basis.ext {ι : Type u_1} {R : Type u_3} {M : Type u_6} [semiring R] [add_comm_monoid M] [module R M] (b : basis ι R M) {R₁ : Type u_10} [semiring R₁] {σ : R →+* R₁} {M₁ : Type u_11} [add_comm_monoid M₁] [module R₁ M₁] {f₁ f₂ : M →ₛₗ[σ] 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_6} [semiring R] [add_comm_monoid M] [module R M] (b : basis ι R M) {R₁ : Type u_10} [semiring R₁] {σ : R →+* R₁} {σ' : R₁ →+* R} [ring_hom_inv_pair σ σ'] [ring_hom_inv_pair σ' σ] {M₁ : Type u_11} [add_comm_monoid M₁] [module R₁ M₁] {f₁ f₂ : M ≃ₛₗ[σ] 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_iff {ι : Type u_1} {R : Type u_3} {M : Type u_6} [semiring R] [add_comm_monoid M] [module R M] (b : basis ι R M) {x y : M} :
x = y (i : ι), ((b.repr) x) i = ((b.repr) y) i

Two elements are equal iff their coordinates are equal.

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

Alias of the reverse direction of basis.ext_elem_iff.

theorem basis.repr_eq_iff {ι : Type u_1} {R : Type u_3} {M : Type u_6} [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_6} [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_6} [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_6} [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_6} [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_6} [semiring R] [add_comm_monoid M] [module R M] {b₁ b₂ : basis ι R M} :
( (i : ι), b₁ i = b₂ i) b₁ = b₂

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

@[protected]
noncomputable def basis.map {ι : Type u_1} {R : Type u_3} {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) (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_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) (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_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) (f : M ≃ₗ[R] M') (i : ι) :
(b.map f) i = f (b i)
@[simp]
theorem basis.map_coeffs_repr {ι : Type u_1} {R : Type u_3} {M : Type u_6} [semiring R] [add_comm_monoid M] [module R M] (b : basis ι R M) {R' : Type u_10} [semiring R'] [module R' M] (f : R ≃+* R') (h : (c : R) (x : M), f c x = c x) :
noncomputable def basis.map_coeffs {ι : Type u_1} {R : Type u_3} {M : Type u_6} [semiring R] [add_comm_monoid M] [module R M] (b : basis ι R M) {R' : Type u_10} [semiring R'] [module R' M] (f : R ≃+* R') (h : (c : R) (x : M), f c x = c x) :
basis ι R' M

If R and R' are isomorphic rings that act identically on a module M, then a basis for M as R-module is also a basis for M as R'-module.

See also basis.algebra_map_coeffs for the case where f is equal to algebra_map.

Equations
theorem basis.map_coeffs_apply {ι : Type u_1} {R : Type u_3} {M : Type u_6} [semiring R] [add_comm_monoid M] [module R M] (b : basis ι R M) {R' : Type u_10} [semiring R'] [module R' M] (f : R ≃+* R') (h : (c : R) (x : M), f c x = c x) (i : ι) :
(b.map_coeffs f h) i = b i
@[simp]
theorem basis.coe_map_coeffs {ι : Type u_1} {R : Type u_3} {M : Type u_6} [semiring R] [add_comm_monoid M] [module R M] (b : basis ι R M) {R' : Type u_10} [semiring R'] [module R' M] (f : R ≃+* R') (h : (c : R) (x : M), f c x = c x) :
noncomputable def basis.reindex {ι : Type u_1} {ι' : Type u_2} {R : Type u_3} {M : Type u_6} [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_6} [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_6} [semiring R] [add_comm_monoid M] [module R M] (b : basis ι R M) (e : ι ι') :
theorem basis.repr_reindex_apply {ι : Type u_1} {ι' : Type u_2} {R : Type u_3} {M : Type u_6} [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.repr_reindex {ι : Type u_1} {ι' : Type u_2} {R : Type u_3} {M : Type u_6} [semiring R] [add_comm_monoid M] [module R M] (b : basis ι R M) (x : M) (e : ι ι') :
@[simp]
theorem basis.reindex_refl {ι : Type u_1} {R : Type u_3} {M : Type u_6} [semiring R] [add_comm_monoid M] [module R M] (b : basis ι R M) :
theorem basis.range_reindex {ι : Type u_1} {ι' : Type u_2} {R : Type u_3} {M : Type u_6} [semiring R] [add_comm_monoid M] [module R M] (b : basis ι R M) (e : ι ι') :

simp can prove this as basis.coe_reindex + equiv_like.range_comp

@[simp]
theorem basis.sum_coords_reindex {ι : Type u_1} {ι' : Type u_2} {R : Type u_3} {M : Type u_6} [semiring R] [add_comm_monoid M] [module R M] (b : basis ι R M) (e : ι ι') :
noncomputable def basis.reindex_range {ι : Type u_1} {R : Type u_3} {M : Type u_6} [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.reindex_range_self {ι : Type u_1} {R : Type u_3} {M : Type u_6} [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_6} [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_6} [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_6} [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_6} [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
noncomputable def basis.reindex_finset_range {ι : Type u_1} {R : Type u_3} {M : Type u_6} [semiring R] [add_comm_monoid M] [module R M] (b : basis ι R M) [fintype ι] [decidable_eq M] :

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_6} [semiring R] [add_comm_monoid M] [module R M] (b : basis ι R M) [fintype ι] [decidable_eq M] (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_6} [semiring R] [add_comm_monoid M] [module R M] (b : basis ι R M) [fintype ι] [decidable_eq M] (x : (finset.image b finset.univ)) :
theorem basis.reindex_finset_range_repr_self {ι : Type u_1} {R : Type u_3} {M : Type u_6} [semiring R] [add_comm_monoid M] [module R M] (b : basis ι R M) [fintype ι] [decidable_eq M] (i : ι) :
@[simp]
theorem basis.reindex_finset_range_repr {ι : Type u_1} {R : Type u_3} {M : Type u_6} [semiring R] [add_comm_monoid M] [module R M] (b : basis ι R M) [fintype ι] [decidable_eq M] (x : M) (i : ι) (h : b i finset.image b finset.univ := _) :
@[protected]
theorem basis.linear_independent {ι : Type u_1} {R : Type u_3} {M : Type u_6} [semiring R] [add_comm_monoid M] [module R M] (b : basis ι R M) :
@[protected]
theorem basis.ne_zero {ι : Type u_1} {R : Type u_3} {M : Type u_6} [semiring R] [add_comm_monoid M] [module R M] (b : basis ι R M) [nontrivial R] (i : ι) :
b i 0
@[protected]
theorem basis.mem_span {ι : Type u_1} {R : Type u_3} {M : Type u_6} [semiring R] [add_comm_monoid M] [module R M] (b : basis ι R M) (x : M) :
@[protected]
theorem basis.span_eq {ι : Type u_1} {R : Type u_3} {M : Type u_6} [semiring R] [add_comm_monoid M] [module R M] (b : basis ι R M) :
theorem basis.index_nonempty {ι : Type u_1} {R : Type u_3} {M : Type u_6} [semiring R] [add_comm_monoid M] [module R M] (b : basis ι R M) [nontrivial M] :
theorem basis.mem_submodule_iff {ι : Type u_1} {R : Type u_3} {M : Type u_6} [semiring R] [add_comm_monoid M] [module R M] {P : submodule R M} (b : basis ι R P) {x : M} :
x P (c : ι →₀ R), x = c.sum (λ (i : ι) (x : R), x (b i))

If the submodule P has a basis, x ∈ P iff it is a linear combination of basis vectors.

noncomputable def basis.constr {ι : Type u_1} {R : Type u_3} {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) (S : Type u_10) [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_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) (S : Type u_10) [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_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) (S : Type u_10) [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_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) (S : Type u_10) [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_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) (S : Type u_10) [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_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) (S : Type u_10) [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_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) (S : Type u_10) [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_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) (S : Type u_10) [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)
@[protected]
noncomputable def basis.equiv {ι : Type u_1} {ι' : Type u_2} {R : Type u_3} {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') (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_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) (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_6} [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_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') (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_6} {M' : Type u_7} {M'' : Type u_8} [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_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') (e : ι ι') :
b.map (b.equiv b' e) = b'.reindex e.symm
@[protected]
noncomputable def basis.prod {ι : Type u_1} {ι' : Type u_2} {R : Type u_3} {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') :
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'. For the specific case of R × R, see also basis.fin_two_prod.

Equations
@[simp]
theorem basis.prod_repr_inl {ι : Type u_1} {ι' : Type u_2} {R : Type u_3} {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') (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_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') (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_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') (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_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') (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_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') (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_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') (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_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') (i : ι ι') :
(b.prod b') i = sum.elim ((linear_map.inl R M M') b) ((linear_map.inr R M M') b') i
@[protected]
theorem basis.no_zero_smul_divisors {ι : Type u_1} {R : Type u_3} {M : Type u_6} [semiring R] [add_comm_monoid M] [module R M] [no_zero_divisors R] (b : basis ι R M) :
@[protected]
theorem basis.smul_eq_zero {ι : Type u_1} {R : Type u_3} {M : Type u_6} [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
theorem eq_bot_of_rank_eq_zero {ι : Type u_1} {R : Type u_3} {M : Type u_6} [semiring R] [add_comm_monoid M] [module R M] [no_zero_divisors R] (b : basis ι R M) (N : submodule R M) (rank_eq : {m : } (v : fin m N), linear_independent R (coe v) m = 0) :
N =
@[protected]
noncomputable 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
@[protected]
noncomputable def basis.empty {ι : Type u_1} {R : Type u_3} (M : Type u_6) [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
@[protected, instance]
noncomputable def basis.empty_unique {ι : Type u_1} {R : Type u_3} (M : Type u_6) [semiring R] [add_comm_monoid M] [module R M] [subsingleton M] [is_empty ι] :
unique (basis ι R M)
Equations
noncomputable def basis.equiv_fun {ι : Type u_1} {R : Type u_3} {M : Type u_6} [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
noncomputable def module.fintype_of_fintype {ι : Type u_1} {R : Type u_3} {M : Type u_6} [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_6} [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_6} [semiring R] [add_comm_monoid M] [module R M] [fintype ι] (b : basis ι R M) (x : ι R) :
(b.equiv_fun.symm) x = finset.univ.sum (λ (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_6} [semiring R] [add_comm_monoid M] [module R M] [fintype ι] (b : basis ι R M) (u : M) :
(b.equiv_fun) u = ((b.repr) u)
@[simp]
theorem basis.map_equiv_fun {ι : Type u_1} {R : Type u_3} {M : Type u_6} {M' : Type u_7} [semiring R] [add_comm_monoid M] [module R M] [add_comm_monoid M'] [module R M'] [fintype ι] (b : basis ι R M) (f : M ≃ₗ[R] M') :
theorem basis.sum_equiv_fun {ι : Type u_1} {R : Type u_3} {M : Type u_6} [semiring R] [add_comm_monoid M] [module R M] [fintype ι] (b : basis ι R M) (u : M) :
finset.univ.sum (λ (i : ι), (b.equiv_fun) u i b i) = u
theorem basis.sum_repr {ι : Type u_1} {R : Type u_3} {M : Type u_6} [semiring R] [add_comm_monoid M] [module R M] [fintype ι] (b : basis ι R M) (u : M) :
finset.univ.sum (λ (i : ι), ((b.repr) u) i b i) = u
@[simp]
theorem basis.equiv_fun_self {ι : Type u_1} {R : Type u_3} {M : Type u_6} [semiring R] [add_comm_monoid M] [module R M] [fintype ι] (b : basis ι R M) [decidable_eq ι] (i j : ι) :
(b.equiv_fun) (b i) j = ite (i = j) 1 0
theorem basis.repr_sum_self {ι : Type u_1} {R : Type u_3} {M : Type u_6} [semiring R] [add_comm_monoid M] [module R M] [fintype ι] (b : basis ι R M) (c : ι R) :
((b.repr) (finset.univ.sum (λ (i : ι), c i b i))) = c
noncomputable def basis.of_equiv_fun {ι : Type u_1} {R : Type u_3} {M : Type u_6} [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_6} [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_6} [semiring R] [add_comm_monoid M] [module R M] [fintype ι] [decidable_eq ι] (e : M ≃ₗ[R] ι R) :
(basis.of_equiv_fun e) = λ (i : ι), (e.symm) (function.update 0 i 1)
@[simp]
theorem basis.of_equiv_fun_equiv_fun {ι : Type u_1} {R : Type u_3} {M : Type u_6} [semiring R] [add_comm_monoid M] [module R M] [fintype ι] (v : basis ι R M) :
@[simp]
theorem basis.equiv_fun_of_equiv_fun {ι : Type u_1} {R : Type u_3} {M : Type u_6} [semiring R] [add_comm_monoid M] [module R M] [fintype ι] (e : M ≃ₗ[R] ι R) :
@[simp]
theorem basis.constr_apply_fintype {ι : Type u_1} {R : Type u_3} {M : Type u_6} {M' : Type u_7} [semiring R] [add_comm_monoid M] [module R M] [add_comm_monoid M'] [module R M'] [fintype ι] (b : basis ι R M) (S : Type u_10) [semiring S] [module S M'] [smul_comm_class R S M'] (f : ι M') (x : M) :
((b.constr S) f) x = finset.univ.sum (λ (i : ι), (b.equiv_fun) x i f i)
theorem basis.mem_submodule_iff' {ι : Type u_1} {R : Type u_3} {M : Type u_6} [semiring R] [add_comm_monoid M] [module R M] [fintype ι] {P : submodule R M} (b : basis ι R P) {x : M} :
x P (c : ι R), x = finset.univ.sum (λ (i : ι), c i (b i))

If the submodule P has a finite basis, x ∈ P iff it is a linear combination of basis vectors.

theorem basis.coord_equiv_fun_symm {ι : Type u_1} {R : Type u_3} {M : Type u_6} [semiring R] [add_comm_monoid M] [module R M] [fintype ι] (b : basis ι R M) (i : ι) (f : ι R) :
(b.coord i) ((b.equiv_fun.symm) f) = f i
noncomputable def basis.equiv' {ι : Type u_1} {ι' : Type u_2} {R : Type u_3} {M : Type u_6} {M' : Type u_7} [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_6} {M' : Type u_7} [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_6} {M' : Type u_7} [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_6} [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 : ι) :
finset.univ.sum (λ (j : ι'), ((b.repr) (b' j)) i * ((b'.repr) x) j) = ((b.repr) x) i
theorem basis.maximal {ι : Type u_1} {R : Type u_3} {M : Type u_6} [ring R] [add_comm_group M] [module R M] [nontrivial R] (b : basis ι R M) :

Any basis is a maximal linear independent set.

@[protected]
noncomputable def basis.mk {ι : Type u_1} {R : Type u_3} {M : Type u_6} {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_6} {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_6} {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_6} {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
theorem basis.mk_coord_apply_eq {ι : Type u_1} {R : Type u_3} {M : Type u_6} {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).coord i) (v i) = 1

Given a basis, the ith element of the dual basis evaluates to 1 on the ith element of the basis.

theorem basis.mk_coord_apply_ne {ι : Type u_1} {R : Type u_3} {M : Type u_6} {v : ι M} [ring R] [add_comm_group M] [module R M] {hli : linear_independent R v} {hsp : submodule.span R (set.range v)} {i j : ι} (h : j i) :
((basis.mk hli hsp).coord i) (v j) = 0

Given a basis, the ith element of the dual basis evaluates to 0 on the jth element of the basis if j ≠ i.

theorem basis.mk_coord_apply {ι : Type u_1} {R : Type u_3} {M : Type u_6} {v : ι M} [ring R] [add_comm_group M] [module R M] {hli : linear_independent R v} {hsp : submodule.span R (set.range v)} [decidable_eq ι] {i j : ι} :
((basis.mk hli hsp).coord i) (v j) = ite (j = i) 1 0

Given a basis, the ith element of the dual basis evaluates to the Kronecker delta on the jth element of the basis.

@[protected]
noncomputable def basis.span {ι : Type u_1} {R : Type u_3} {M : Type u_6} {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
@[protected]
theorem basis.span_apply {ι : Type u_1} {R : Type u_3} {M : Type u_6} {v : ι M} [ring R] [add_comm_group M] [module R M] (hli : linear_independent R v) (i : ι) :
((basis.span hli) i) = v i
theorem basis.group_smul_span_eq_top {ι : Type u_1} {R : Type u_3} {M : Type u_6} [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} :
noncomputable def basis.group_smul {ι : Type u_1} {R : Type u_3} {M : Type u_6} [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_6} [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_6} [ring R] [add_comm_group M] [module R M] {v : ι M} (hv : submodule.span R (set.range v) = ) {w : ι Rˣ} :
noncomputable def basis.units_smul {ι : Type u_1} {R : Type u_3} {M : Type u_6} [ring R] [add_comm_group M] [module R M] (v : basis ι R M) (w : ι 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_6} [ring R] [add_comm_group M] [module R M] {v : basis ι R M} {w : ι Rˣ} (i : ι) :
(v.units_smul w) i = w i v i
@[simp]
theorem basis.coord_units_smul {ι : Type u_1} {R₂ : Type u_4} {M : Type u_6} [comm_ring R₂] [add_comm_group M] [module R₂ M] (e : basis ι R₂ M) (w : ι R₂ˣ) (i : ι) :
(e.units_smul w).coord i = (w i)⁻¹ e.coord i
@[simp]
theorem basis.repr_units_smul {ι : Type u_1} {R₂ : Type u_4} {M : Type u_6} [comm_ring R₂] [add_comm_group M] [module R₂ M] (e : basis ι R₂ M) (w : ι R₂ˣ) (v : M) (i : ι) :
(((e.units_smul w).repr) v) i = (w i)⁻¹ ((e.repr) v) i
noncomputable def basis.is_unit_smul {ι : Type u_1} {R : Type u_3} {M : Type u_6} [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_6} [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
noncomputable def basis.mk_fin_cons {R : Type u_3} {M : Type u_6} [ring R] [add_comm_group M] [module R M] {n : } {N : submodule R M} (y : M) (b : basis (fin n) R N) (hli : (c : R) (x : M), x N c y + x = 0 c = 0) (hsp : (z : M), (c : R), z + c y N) :
basis (fin (n + 1)) R M

Let b be a basis for a submodule N of M. If y : M is linear independent of N and y and N together span the whole of M, then there is a basis for M whose basis vectors are given by fin.cons y b.

Equations
@[simp]
theorem basis.coe_mk_fin_cons {R : Type u_3} {M : Type u_6} [ring R] [add_comm_group M] [module R M] {n : } {N : submodule R M} (y : M) (b : basis (fin n) R N) (hli : (c : R) (x : M), x N c y + x = 0 c = 0) (hsp : (z : M), (c : R), z + c y N) :
noncomputable def basis.mk_fin_cons_of_le {R : Type u_3} {M : Type u_6} [ring R] [add_comm_group M] [module R M] {n : } {N O : submodule R M} (y : M) (yO : y O) (b : basis (fin n) R N) (hNO : N O) (hli : (c : R) (x : M), x N c y + x = 0 c = 0) (hsp : (z : M), z O ( (c : R), z + c y N)) :
basis (fin (n + 1)) R O

Let b be a basis for a submodule N ≤ O. If y ∈ O is linear independent of N and y and N together span the whole of O, then there is a basis for O whose basis vectors are given by fin.cons y b.

Equations
@[simp]
theorem basis.coe_mk_fin_cons_of_le {R : Type u_3} {M : Type u_6} [ring R] [add_comm_group M] [module R M] {n : } {N O : submodule R M} (y : M) (yO : y O) (b : basis (fin n) R N) (hNO : N O) (hli : (c : R) (x : M), x N c y + x = 0 c = 0) (hsp : (z : M), z O ( (c : R), z + c y N)) :
(basis.mk_fin_cons_of_le y yO b hNO hli hsp) = fin.cons y, yO⟩ ((submodule.of_le hNO) b)
@[protected]
noncomputable def basis.fin_two_prod (R : Type u_1) [semiring R] :
basis (fin 2) R (R × R)

The basis of R × R given by the two vectors (1, 0) and (0, 1).

Equations
@[simp]
theorem basis.fin_two_prod_zero (R : Type u_1) [semiring R] :
@[simp]
theorem basis.fin_two_prod_one (R : Type u_1) [semiring R] :
@[simp]
theorem basis.coe_fin_two_prod_repr {R : Type u_1} [semiring R] (x : R × R) :
def submodule.induction_on_rank_aux {ι : Type u_1} {R : Type u_3} {M : Type u_6} [ring R] [is_domain R] [add_comm_group M] [module R M] (b : basis ι R M) (P : submodule R M Sort u_2) (ih : Π (N : submodule R M), (Π (N' : submodule R M), N' N Π (x : M), x N ( (c : R) (y : M), y N' c x + y = 0 c = 0) P N') P N) (n : ) (N : submodule R M) (rank_le : {m : } (v : fin m N), linear_independent R (coe v) m n) :
P N

If N is a submodule with finite rank, do induction on adjoining a linear independent element to a submodule.

Equations
noncomputable def basis.extend {K : Type u_5} {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_5} {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_5} {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_5} {V : Type u} [division_ring K] [add_comm_group V] [module K V] {s : set V} (hs : linear_independent K coe) :
noncomputable def basis.sum_extend {ι : Type u_1} {K : Type u_5} {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_5} {V : Type u} [division_ring K] [add_comm_group V] [module K V] {s : set V} (hs : linear_independent K coe) :
s hs.extend _
noncomputable def basis.of_vector_space (K : Type u_5) (V : Type u) [division_ring K] [add_comm_group V] [module K V] :

Each vector space has a basis.

Equations
@[simp]
theorem basis.exists_basis (K : Type u_5) (V : Type u) [division_ring K] [add_comm_group V] [module K V] :
(s : set V), nonempty (basis s K V)
theorem nonzero_span_atom {K : Type u_5} {V : Type u} [division_ring K] [add_comm_group V] [module K V] (v : V) (hv : v 0) :

For a module over a division ring, the span of a nonzero element is an atom of the lattice of submodules.

theorem atom_iff_nonzero_span {K : Type u_5} {V : Type u} [division_ring K] [add_comm_group V] [module K V] (W : submodule K V) :
is_atom W (v : V) (hv : v 0), W = submodule.span K {v}

The atoms of the lattice of submodules of a module over a division ring are the submodules equal to the span of a nonzero element of the module.

@[protected, instance]

The lattice of submodules of a module over a division ring is atomistic.

theorem linear_map.exists_left_inverse_of_injective {K : Type u_5} {V : Type u} {V' : Type u_9} [division_ring K] [add_comm_group V] [add_comm_group V'] [module K V] [module K V'] (f : V →ₗ[K] V') (hf_inj : linear_map.ker f = ) :
(g : V' →ₗ[K] V), g.comp f = linear_map.id
theorem submodule.exists_is_compl {K : Type u_5} {V : Type u} [division_ring K] [add_comm_group V] [module K V] (p : submodule K V) :
(q : submodule K V), is_compl p q
@[protected, instance]
theorem linear_map.exists_right_inverse_of_surjective {K : Type u_5} {V : Type u} {V' : Type u_9} [division_ring K] [add_comm_group V] [add_comm_group V'] [module K V] [module K V'] (f : V →ₗ[K] V') (hf_surj : linear_map.range f = ) :
(g : V' →ₗ[K] V), f.comp g = linear_map.id
theorem linear_map.exists_extend {K : Type u_5} {V : Type u} {V' : Type u_9} [division_ring 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_5} {V : Type u} [division_ring K] [add_comm_group V] [module K V] (p : submodule K V) (hp : p < ) :
(f : V →ₗ[K] K) (H : f 0), p linear_map.ker f

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_5} {V : Type u} [division_ring K] [add_comm_group V] [module K V] (p : submodule K V) :
nonempty (((V p) × p) ≃ₗ[K] V)
noncomputable def basis.restrict_scalars {ι : Type u_1} (R : Type u_3) {M : Type u_6} {S : Type u_10} [comm_ring R] [ring S] [nontrivial S] [add_comm_group M] [algebra R S] [module S M] [module R M] [is_scalar_tower R S M] [no_zero_smul_divisors R S] (b : basis ι S M) :

Let b be a S-basis of M. Let R be a comm_ring such that algebra R S with no zero smul divisors, then the submodule of M spanned by b over R admits b as a R-basis.

Equations
@[simp]
theorem basis.restrict_scalars_apply {ι : Type u_1} (R : Type u_3) {M : Type u_6} {S : Type u_10} [comm_ring R] [ring S] [nontrivial S] [add_comm_group M] [algebra R S] [module S M] [module R M] [is_scalar_tower R S M] [no_zero_smul_divisors R S] (b : basis ι S M) (i : ι) :
@[simp]
theorem basis.restrict_scalars_repr_apply {ι : Type u_1} (R : Type u_3) {M : Type u_6} {S : Type u_10} [comm_ring R] [ring S] [nontrivial S] [add_comm_group M] [algebra R S] [module S M] [module R M] [is_scalar_tower R S M] [no_zero_smul_divisors R S] (b : basis ι S M) (m : (submodule.span R (set.range b))) (i : ι) :
theorem basis.mem_span_iff_repr_mem {ι : Type u_1} (R : Type u_3) {M : Type u_6} {S : Type u_10} [comm_ring R] [ring S] [nontrivial S] [add_comm_group M] [algebra R S] [module S M] [module R M] [is_scalar_tower R S M] [no_zero_smul_divisors R S] (b : basis ι S M) (m : M) :

Let b be a S-basis of M. Then m : M lies in the R-module spanned by b iff all the coordinates of m on the basis b are in R (see basis.mem_span for the case R = S).