mathlib documentation

linear_algebra.finsupp_vector_space

theorem finsupp.linear_independent_single {R : Type u_1} {M : Type u_2} {ι : Type u_3} [ring R] [add_comm_group M] [module R M] {φ : ι → Type u_4} {f : Π (ι : ι), φ ι → M} :
(∀ (i : ι), linear_independent R (f i))linear_independent R (λ (ix : Σ (i : ι), φ i), finsupp.single ix.fst (f ix.fst ix.snd))

theorem finsupp.is_basis_single {R : Type u_1} {M : Type u_2} {ι : Type u_3} [ring R] [add_comm_group M] [module R M] {φ : ι → Type u_4} (f : Π (ι : ι), φ ι → M) :
(∀ (i : ι), is_basis R (f i))is_basis R (λ (ix : Σ (i : ι), φ i), finsupp.single ix.fst (f ix.fst ix.snd))

theorem finsupp.is_basis_single_one {R : Type u_1} {ι : Type u_3} [ring R] :
is_basis R (λ (i : ι), finsupp.single i 1)

theorem finsupp.is_basis.tensor_product {R : Type u_1} {M : Type u_2} {N : Type u_3} {ι : Type u_4} {κ : Type u_5} [comm_ring R] [add_comm_group M] [module R M] [add_comm_group N] [module R N] {b : ι → M} (hb : is_basis R b) {c : κ → N} :
is_basis R cis_basis R (λ (i : ι × κ), b i.fst ⊗ₜ[R] c i.snd)

If b : ι → M and c : κ → N are bases then so is λ i, b i.1 ⊗ₜ c i.2 : ι × κ → M ⊗ N.

theorem finsupp.dim_eq {K : Type u} {V ι : Type v} [field K] [add_comm_group V] [vector_space K V] :

theorem equiv_of_dim_eq_lift_dim {K : Type u} {V : Type v} {V' : Type w} [field K] [add_comm_group V] [vector_space K V] [add_comm_group V'] [vector_space K V'] :

def equiv_of_dim_eq_dim {K : Type u} {V₁ V₂ : Type v} [field K] [add_comm_group V₁] [vector_space K V₁] [add_comm_group V₂] [vector_space K V₂] :
vector_space.dim K V₁ = vector_space.dim K V₂(V₁ ≃ₗ[K] V₂)

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

Equations
def fin_dim_vectorspace_equiv {K : Type u} {V : Type v} [field K] [add_comm_group V] [vector_space K V] (n : ) :
vector_space.dim K V = n(V ≃ₗ[K] fin n → K)

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

Equations
theorem eq_bot_iff_dim_eq_zero {K : Type u} {V : Type v} [field K] [add_comm_group V] [vector_space K V] (p : submodule K V) :

theorem injective_of_surjective {K : Type u} {V₁ V₂ : Type v} [field K] [add_comm_group V₁] [vector_space K V₁] [add_comm_group V₂] [vector_space K V₂] (f : V₁ →ₗ[K] V₂) :