# mathlibdocumentation

linear_algebra.finsupp_vector_space

# Linear structures on function with finite support ι →₀ M#

This file contains results on the R-module structure on functions of finite support from a type ι to an R-module M, in particular in the case that R is a field.

Furthermore, it contains some facts about isomorphisms of vector spaces from equality of dimension as well as the cardinality of finite dimensional vector spaces.

## TODO #

Move the second half of this file to more appropriate other files.

theorem finsupp.linear_independent_single {R : Type u_1} {M : Type u_2} {ι : Type u_3} [ring R] [ M] {φ : ι → Type u_4} {f : Π (ι : ι), φ ι → M} (hf : ∀ (i : ι), (f i)) :
(λ (ix : Σ (i : ι), φ i), (f ix.fst ix.snd))
@[protected]
noncomputable def finsupp.basis {R : Type u_1} {M : Type u_2} {ι : Type u_3} [semiring R] [ M] {φ : ι → Type u_4} (b : Π (i : ι), basis (φ i) R M) :
basis (Σ (i : ι), φ i) R →₀ M)

The basis on ι →₀ M with basis vectors λ ⟨i, x⟩, single i (b i x).

Equations
@[simp]
theorem finsupp.basis_repr {R : Type u_1} {M : Type u_2} {ι : Type u_3} [semiring R] [ M] {φ : ι → Type u_4} (b : Π (i : ι), basis (φ i) R M) (g : ι →₀ M) (ix : Σ (i : ι), φ i) :
(((finsupp.basis b).repr) g) ix = (((b ix.fst).repr) (g ix.fst)) ix.snd
@[simp]
theorem finsupp.coe_basis {R : Type u_1} {M : Type u_2} {ι : Type u_3} [semiring R] [ M] {φ : ι → Type u_4} (b : Π (i : ι), basis (φ i) R M) :
= λ (ix : Σ (i : ι), φ i), ((b ix.fst) ix.snd)
@[protected]
noncomputable def finsupp.basis_single_one {R : Type u_1} {ι : Type u_3} [semiring R] :
R →₀ R)

The basis on ι →₀ M with basis vectors λ i, single i 1.

Equations
@[simp]
theorem finsupp.basis_single_one_repr {R : Type u_1} {ι : Type u_3} [semiring R] :
@[simp]
theorem finsupp.coe_basis_single_one {R : Type u_1} {ι : Type u_3} [semiring R] :
theorem finsupp.dim_eq {K : Type u} {V ι : Type v} [field K] [ V] :
→₀ V) = * V
theorem equiv_of_dim_eq_lift_dim {K : Type u} {V : Type v} {V' : Type w} [field K] [ V] [add_comm_group V'] [ V'] (h : V).lift = V').lift) :
noncomputable def equiv_of_dim_eq_dim {K : Type u} {V₁ V₂ : Type v} [field K] [add_comm_group V₁] [ V₁] [add_comm_group V₂] [ V₂] (h : V₁ = V₂) :
V₁ ≃ₗ[K] V₂

Two K-vector spaces are equivalent if their dimension is the same.

Equations
noncomputable def fin_dim_vectorspace_equiv {K : Type u} {V : Type v} [field K] [ V] (n : ) (hn : V = n) :
V ≃ₗ[K] fin n → K

An n-dimensional K-vector space is equivalent to fin n → K.

Equations
theorem cardinal_mk_eq_cardinal_mk_field_pow_dim (K V : Type u) [field K] [ V] [ V] :
= ^ V
theorem cardinal_lt_aleph_0_of_finite_dimensional (K V : Type u) [field K] [ V] [fintype K] [ V] :