# mathlib3documentation

linear_algebra.finsupp_vector_space

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

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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.

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] :

TODO: move this section to an earlier file.

theorem finset.sum_single_ite {R : Type u_1} {n : Type u_3} [decidable_eq n] [fintype n] [semiring R] (a : R) (i : n) :
finset.univ.sum (λ (x : n), (ite (i = x) a 0)) =
@[simp]
theorem basis.equiv_fun_symm_std_basis {R : Type u_1} {M : Type u_2} {n : Type u_3} [decidable_eq n] [fintype n] [semiring R] [ M] (b : R M) (i : n) :
(b.equiv_fun.symm) ( (λ (_x : n), R) i) 1) = b i