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}
(hf : ∀ (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)
(hf : ∀ (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}
(hc : is_basis R c) :
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] :
vector_space.dim K (ι →₀ V) = (# ι) * vector_space.dim 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']
(h : (vector_space.dim K V).lift = (vector_space.dim K V').lift) :
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₂]
(h : vector_space.dim K V₁ = vector_space.dim 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 : ℕ)
(hn : vector_space.dim K V = ↑n) :
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)
(h : vector_space.dim K ↥p = 0) :
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₂)
(hV₁ : vector_space.dim K V₁ < cardinal.omega)
(heq : vector_space.dim K V₂ = vector_space.dim K V₁)
(hf : f.range = ⊤) :
theorem
cardinal_mk_eq_cardinal_mk_field_pow_dim
{K V : Type u}
[field K]
[add_comm_group V]
[vector_space K V]
(h : vector_space.dim K V < cardinal.omega) :
# V = # K ^ vector_space.dim K V
theorem
cardinal_lt_omega_of_dim_lt_omega
{K V : Type u}
[field K]
[add_comm_group V]
[vector_space K V]
[fintype K]
(h : vector_space.dim K V < cardinal.omega) :
# V < cardinal.omega