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) :
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} :
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) = cardinal.mk ι * 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'] :
(vector_space.dim K V).lift = (vector_space.dim K V').lift → nonempty (V ≃ₗ[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₂)
Equations
def
fin_dim_vectorspace_equiv
{K : Type u}
{V : Type v}
[field K]
[add_comm_group V]
[vector_space K V]
(n : ℕ) :
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) :
vector_space.dim K ↥p = 0 → p = ⊥
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₂) :
vector_space.dim K V₁ < cardinal.omega → vector_space.dim K V₂ = vector_space.dim K V₁ → f.range = ⊤ → f.ker = ⊥
theorem
cardinal_mk_eq_cardinal_mk_field_pow_dim
{K V : Type u}
[field K]
[add_comm_group V]
[vector_space K V] :
vector_space.dim K V < cardinal.omega → cardinal.mk V = cardinal.mk 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] :