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.

Instances for basis
@[protected, instance]
noncomputable def basis.inhabited {ι : Type u_1} {R : Type u_3} [semiring R] :
inhabited (basis ι R →₀ R))
Equations
@[protected, instance]
noncomputable 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] :
has_coe_to_fun (basis ι R M) (λ (_x : basis ι R M), ι → 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)
@[protected]
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) :
theorem basis.mem_span_repr_support {R : Type u_3} {M : Type u_5} [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_5} [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_5} [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_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
noncomputable def basis.sum_coords {ι : Type u_1} {R : Type u_3} {M : Type u_5} [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_5} [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_5} [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_5} [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_5} [semiring R] [add_comm_monoid M] [module R M] (b : basis ι R M) (i : ι) :
(b.sum_coords) (b i) = 1
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) {R₁ : Type u_9} [semiring R₁] {σ : R →+* R₁} {M₁ : Type u_10} [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_5} [semiring R] [add_comm_monoid M] [module R M] (b : basis ι R M) {R₁ : Type u_9} [semiring R₁] {σ : R →+* R₁} {σ' : R₁ →+* R} [ring_hom_inv_pair σ σ'] [ring_hom_inv_pair σ' σ] {M₁ : Type u_10} [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 {ι : 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.

@[protected]
noncomputable 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)
@[simp]
theorem basis.map_coeffs_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) {R' : Type u_9} [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_5} [semiring R] [add_comm_monoid M] [module R M] (b : basis ι R M) {R' : Type u_9} [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_5} [semiring R] [add_comm_monoid M] [module R M] (b : basis ι R M) {R' : Type u_9} [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_5} [semiring R] [add_comm_monoid M] [module R M] (b : basis ι R M) {R' : Type u_9} [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_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.reindex_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.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 : ι ι') :
noncomputable 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
noncomputable 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 := _) :
@[protected]
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) :
@[protected]
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
@[protected]
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) :
@[protected]
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) :
theorem basis.index_nonempty {ι : 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 M] :
noncomputable 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)
@[protected]
noncomputable 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
@[protected]
noncomputable 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'. 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_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
@[protected]
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) :
@[protected]
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
theorem eq_bot_of_rank_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) (N : submodule R M) (rank_eq : ∀ {m : } (v : fin mN), 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_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
@[protected, instance]
noncomputable 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
noncomputable 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
noncomputable 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 = 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_5} [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_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) (f : M ≃ₗ[R] M') :
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) :
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_5} [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_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
noncomputable 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.of_equiv_fun_equiv_fun {ι : Type u_1} {R : Type u_3} {M : Type u_5} [semiring R] [add_comm_monoid M] [module R M] [fintype ι] (v : basis ι R M) :
@[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 = finset.univ.sum (λ (i : ι), (b.equiv_fun) x i f i)
noncomputable 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 : ι) :
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_5} [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_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
theorem basis.mk_coord_apply_eq {ι : 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).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_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 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_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 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_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
@[protected]
theorem basis.span_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) (i : ι) :
((basis.span hli) i) = v i
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} :
noncomputable 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 : ι → Rˣ} :
noncomputable 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 : ι → 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 : ι → Rˣ} (i : ι) :
(v.units_smul w) i = w i v i
noncomputable 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
noncomputable def basis.mk_fin_cons {R : Type u_3} {M : Type u_5} [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 Nc y + x = 0c = 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_5} [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 Nc y + x = 0c = 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_5} [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 Nc y + x = 0c = 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_5} [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 Nc y + x = 0c = 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_5} [ring R] [is_domain R] [add_comm_group M] [module R M] (b : basis ι R M) (P : submodule R MSort 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 = 0c = 0)P N')P N) (n : ) (N : submodule R M) (rank_le : ∀ {m : } (v : fin mN), 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_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) :
noncomputable 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 _
noncomputable 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 nonzero_span_atom {K : Type u_4} {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_4} {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]
def submodule.is_atomistic {K : Type u_4} {V : Type u} [division_ring K] [add_comm_group V] [module K V] :

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

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 : linear_map.ker f = ) :
∃ (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
@[protected, instance]
def module.submodule.complemented_lattice {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 : linear_map.range f = ) :
∃ (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 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_4} {V : Type u} [field K] [add_comm_group V] [module K V] (p : submodule K V) :
nonempty (((V p) × p) ≃ₗ[K] V)