`Finsupp.linearCombination` #

Main definitions #

Finsupp.linearCombination R (v : ι → M): sends l : ι → R to the linear combination of v i with coefficients l i;
Finsupp.linearCombinationOn: a restricted version of Finsupp.linearCombination with domain

Tags #

function with finite support, module, linear algebra

def Finsupp.linearCombination {α : Type u_1} {M : Type u_2} (R : Type u_5) [Semiring R] [AddCommMonoid M] [Module R M] (v : α → M) :

(α →₀ R) →ₗ[R] M

Interprets (l : α →₀ R) as a linear combination of the elements in the family (v : α → M) and evaluates this linear combination.

Equations

Finsupp.linearCombination R v = (Finsupp.lsum ℕ) fun (i : α) => LinearMap.id.smulRight (v i)

Instances For

source

@[deprecated Finsupp.linearCombination (since := "2024-08-29")]

def Finsupp.total {α : Type u_1} {M : Type u_2} (R : Type u_5) [Semiring R] [AddCommMonoid M] [Module R M] (v : α → M) :

(α →₀ R) →ₗ[R] M

Alias of Finsupp.linearCombination.

Interprets (l : α →₀ R) as a linear combination of the elements in the family (v : α → M) and evaluates this linear combination.

Equations

@Finsupp.total = @Finsupp.linearCombination

Instances For

source

theorem Finsupp.linearCombination_apply {α : Type u_1} {M : Type u_2} (R : Type u_5) [Semiring R] [AddCommMonoid M] [Module R M] {v : α → M} (l : α →₀ R) :

(Finsupp.linearCombination R v) l = l.sum fun (i : α) (a : R) => a • v i

source

@[deprecated Finsupp.linearCombination_apply (since := "2024-08-29")]

theorem Finsupp.total_apply {α : Type u_1} {M : Type u_2} (R : Type u_5) [Semiring R] [AddCommMonoid M] [Module R M] {v : α → M} (l : α →₀ R) :

(Finsupp.linearCombination R v) l = l.sum fun (i : α) (a : R) => a • v i

Alias of Finsupp.linearCombination_apply.

source

theorem Finsupp.linearCombination_apply_of_mem_supported {α : Type u_1} {M : Type u_2} (R : Type u_5) [Semiring R] [AddCommMonoid M] [Module R M] {v : α → M} {l : α →₀ R} {s : Finset α} (hs : l ∈ Finsupp.supported R R ↑s) :

(Finsupp.linearCombination R v) l = ∑ i ∈ s, l i • v i

source

@[deprecated Finsupp.linearCombination_apply_of_mem_supported (since := "2024-08-29")]

theorem Finsupp.total_apply_of_mem_supported {α : Type u_1} {M : Type u_2} (R : Type u_5) [Semiring R] [AddCommMonoid M] [Module R M] {v : α → M} {l : α →₀ R} {s : Finset α} (hs : l ∈ Finsupp.supported R R ↑s) :

(Finsupp.linearCombination R v) l = ∑ i ∈ s, l i • v i

Alias of Finsupp.linearCombination_apply_of_mem_supported.

source

@[simp]

theorem Finsupp.linearCombination_single {α : Type u_1} {M : Type u_2} (R : Type u_5) [Semiring R] [AddCommMonoid M] [Module R M] {v : α → M} (c : R) (a : α) :

(Finsupp.linearCombination R v) (Finsupp.single a c) = c • v a

source

@[deprecated Finsupp.linearCombination_single (since := "2024-08-29")]

theorem Finsupp.total_single {α : Type u_1} {M : Type u_2} (R : Type u_5) [Semiring R] [AddCommMonoid M] [Module R M] {v : α → M} (c : R) (a : α) :

(Finsupp.linearCombination R v) (Finsupp.single a c) = c • v a

Alias of Finsupp.linearCombination_single.

source

theorem Finsupp.linearCombination_zero_apply {α : Type u_1} {M : Type u_2} (R : Type u_5) [Semiring R] [AddCommMonoid M] [Module R M] (x : α →₀ R) :

(Finsupp.linearCombination R 0) x = 0

source

@[deprecated Finsupp.linearCombination_zero_apply (since := "2024-08-29")]

theorem Finsupp.total_zero_apply {α : Type u_1} {M : Type u_2} (R : Type u_5) [Semiring R] [AddCommMonoid M] [Module R M] (x : α →₀ R) :

(Finsupp.linearCombination R 0) x = 0

Alias of Finsupp.linearCombination_zero_apply.

source

@[simp]

theorem Finsupp.linearCombination_zero (α : Type u_1) (M : Type u_2) (R : Type u_5) [Semiring R] [AddCommMonoid M] [Module R M] :

Finsupp.linearCombination R 0 = 0

source

@[deprecated Finsupp.linearCombination_zero (since := "2024-08-29")]

theorem Finsupp.total_zero (α : Type u_1) (M : Type u_2) (R : Type u_5) [Semiring R] [AddCommMonoid M] [Module R M] :

Finsupp.linearCombination R 0 = 0

Alias of Finsupp.linearCombination_zero.

source

theorem Finsupp.linearCombination_linear_comp {α : Type u_1} {M : Type u_2} (R : Type u_5) [Semiring R] [AddCommMonoid M] [Module R M] {M' : Type u_8} [AddCommMonoid M'] [Module R M'] {v : α → M} (f : M →ₗ[R] M') :

Finsupp.linearCombination R (⇑f ∘ v) = f ∘ₗ Finsupp.linearCombination R v

source

theorem Finsupp.apply_linearCombination {α : Type u_1} {M : Type u_2} (R : Type u_5) [Semiring R] [AddCommMonoid M] [Module R M] {M' : Type u_8} [AddCommMonoid M'] [Module R M'] (f : M →ₗ[R] M') (v : α → M) (l : α →₀ R) :

f ((Finsupp.linearCombination R v) l) = (Finsupp.linearCombination R (⇑f ∘ v)) l

source

@[deprecated Finsupp.apply_linearCombination (since := "2024-08-29")]

theorem Finsupp.apply_total {α : Type u_1} {M : Type u_2} (R : Type u_5) [Semiring R] [AddCommMonoid M] [Module R M] {M' : Type u_8} [AddCommMonoid M'] [Module R M'] (f : M →ₗ[R] M') (v : α → M) (l : α →₀ R) :

f ((Finsupp.linearCombination R v) l) = (Finsupp.linearCombination R (⇑f ∘ v)) l

Alias of Finsupp.apply_linearCombination.

source

theorem Finsupp.apply_linearCombination_id {M : Type u_2} (R : Type u_5) [Semiring R] [AddCommMonoid M] [Module R M] {M' : Type u_8} [AddCommMonoid M'] [Module R M'] (f : M →ₗ[R] M') (l : M →₀ R) :

f ((Finsupp.linearCombination R id) l) = (Finsupp.linearCombination R ⇑f) l

source

@[deprecated Finsupp.apply_linearCombination_id (since := "2024-08-29")]

theorem Finsupp.apply_total_id {M : Type u_2} (R : Type u_5) [Semiring R] [AddCommMonoid M] [Module R M] {M' : Type u_8} [AddCommMonoid M'] [Module R M'] (f : M →ₗ[R] M') (l : M →₀ R) :

f ((Finsupp.linearCombination R id) l) = (Finsupp.linearCombination R ⇑f) l

Alias of Finsupp.apply_linearCombination_id.

source

theorem Finsupp.linearCombination_unique {α : Type u_1} {M : Type u_2} (R : Type u_5) [Semiring R] [AddCommMonoid M] [Module R M] [Unique α] (l : α →₀ R) (v : α → M) :

(Finsupp.linearCombination R v) l = l default • v default

source

@[deprecated Finsupp.linearCombination_unique (since := "2024-08-29")]

theorem Finsupp.total_unique {α : Type u_1} {M : Type u_2} (R : Type u_5) [Semiring R] [AddCommMonoid M] [Module R M] [Unique α] (l : α →₀ R) (v : α → M) :

(Finsupp.linearCombination R v) l = l default • v default

Alias of Finsupp.linearCombination_unique.

source

theorem Finsupp.linearCombination_surjective {α : Type u_1} {M : Type u_2} (R : Type u_5) [Semiring R] [AddCommMonoid M] [Module R M] {v : α → M} (h : Function.Surjective v) :

Function.Surjective ⇑(Finsupp.linearCombination R v)

source

@[deprecated Finsupp.linearCombination_surjective (since := "2024-08-29")]

theorem Finsupp.total_surjective {α : Type u_1} {M : Type u_2} (R : Type u_5) [Semiring R] [AddCommMonoid M] [Module R M] {v : α → M} (h : Function.Surjective v) :

Function.Surjective ⇑(Finsupp.linearCombination R v)

Alias of Finsupp.linearCombination_surjective.

source

theorem Finsupp.linearCombination_range {α : Type u_1} {M : Type u_2} (R : Type u_5) [Semiring R] [AddCommMonoid M] [Module R M] {v : α → M} (h : Function.Surjective v) :

LinearMap.range (Finsupp.linearCombination R v) = ⊤

source

@[deprecated Finsupp.linearCombination_range (since := "2024-08-29")]

theorem Finsupp.total_range {α : Type u_1} {M : Type u_2} (R : Type u_5) [Semiring R] [AddCommMonoid M] [Module R M] {v : α → M} (h : Function.Surjective v) :

LinearMap.range (Finsupp.linearCombination R v) = ⊤

Alias of Finsupp.linearCombination_range.

source

theorem Finsupp.linearCombination_id_surjective (R : Type u_5) [Semiring R] (M : Type u_9) [AddCommMonoid M] [Module R M] :

Function.Surjective ⇑(Finsupp.linearCombination R id)

Any module is a quotient of a free module. This is stated as surjectivity of Finsupp.linearCombination R id : (M →₀ R) →ₗ[R] M.

source

@[deprecated Finsupp.linearCombination_id_surjective (since := "2024-08-29")]

theorem Finsupp.total_id_surjective (R : Type u_5) [Semiring R] (M : Type u_9) [AddCommMonoid M] [Module R M] :

Function.Surjective ⇑(Finsupp.linearCombination R id)

Alias of Finsupp.linearCombination_id_surjective.

Any module is a quotient of a free module. This is stated as surjectivity of Finsupp.linearCombination R id : (M →₀ R) →ₗ[R] M.

source

theorem Finsupp.range_linearCombination {α : Type u_1} {M : Type u_2} (R : Type u_5) [Semiring R] [AddCommMonoid M] [Module R M] {v : α → M} :

LinearMap.range (Finsupp.linearCombination R v) = Submodule.span R (Set.range v)

source

@[deprecated Finsupp.range_linearCombination (since := "2024-08-29")]

theorem Finsupp.range_total {α : Type u_1} {M : Type u_2} (R : Type u_5) [Semiring R] [AddCommMonoid M] [Module R M] {v : α → M} :

LinearMap.range (Finsupp.linearCombination R v) = Submodule.span R (Set.range v)

Alias of Finsupp.range_linearCombination.

source

theorem Finsupp.lmapDomain_linearCombination {α : Type u_1} {M : Type u_2} (R : Type u_5) [Semiring R] [AddCommMonoid M] [Module R M] {α' : Type u_7} {M' : Type u_8} [AddCommMonoid M'] [Module R M'] {v : α → M} {v' : α' → M'} (f : α → α') (g : M →ₗ[R] M') (h : ∀ (i : α), g (v i) = v' (f i)) :

Finsupp.linearCombination R v' ∘ₗ Finsupp.lmapDomain R R f = g ∘ₗ Finsupp.linearCombination R v

source

@[deprecated Finsupp.lmapDomain_linearCombination (since := "2024-08-29")]

theorem Finsupp.lmapDomain_total {α : Type u_1} {M : Type u_2} (R : Type u_5) [Semiring R] [AddCommMonoid M] [Module R M] {α' : Type u_7} {M' : Type u_8} [AddCommMonoid M'] [Module R M'] {v : α → M} {v' : α' → M'} (f : α → α') (g : M →ₗ[R] M') (h : ∀ (i : α), g (v i) = v' (f i)) :

Finsupp.linearCombination R v' ∘ₗ Finsupp.lmapDomain R R f = g ∘ₗ Finsupp.linearCombination R v

Alias of Finsupp.lmapDomain_linearCombination.

source

theorem Finsupp.linearCombination_comp_lmapDomain {α : Type u_1} (R : Type u_5) [Semiring R] {α' : Type u_7} {M' : Type u_8} [AddCommMonoid M'] [Module R M'] {v' : α' → M'} (f : α → α') :

Finsupp.linearCombination R v' ∘ₗ Finsupp.lmapDomain R R f = Finsupp.linearCombination R (v' ∘ f)

source

@[deprecated Finsupp.linearCombination_comp_lmapDomain (since := "2024-08-29")]

theorem Finsupp.total_comp_lmapDomain {α : Type u_1} (R : Type u_5) [Semiring R] {α' : Type u_7} {M' : Type u_8} [AddCommMonoid M'] [Module R M'] {v' : α' → M'} (f : α → α') :

Finsupp.linearCombination R v' ∘ₗ Finsupp.lmapDomain R R f = Finsupp.linearCombination R (v' ∘ f)

Alias of Finsupp.linearCombination_comp_lmapDomain.

source

@[simp]

theorem Finsupp.linearCombination_embDomain {α : Type u_1} (R : Type u_5) [Semiring R] {α' : Type u_7} {M' : Type u_8} [AddCommMonoid M'] [Module R M'] {v' : α' → M'} (f : α ↪ α') (l : α →₀ R) :

(Finsupp.linearCombination R v') (Finsupp.embDomain f l) = (Finsupp.linearCombination R (v' ∘ ⇑f)) l

source

@[deprecated Finsupp.linearCombination_embDomain (since := "2024-08-29")]

theorem Finsupp.total_embDomain {α : Type u_1} (R : Type u_5) [Semiring R] {α' : Type u_7} {M' : Type u_8} [AddCommMonoid M'] [Module R M'] {v' : α' → M'} (f : α ↪ α') (l : α →₀ R) :

(Finsupp.linearCombination R v') (Finsupp.embDomain f l) = (Finsupp.linearCombination R (v' ∘ ⇑f)) l

Alias of Finsupp.linearCombination_embDomain.

source

@[simp]

theorem Finsupp.linearCombination_mapDomain {α : Type u_1} (R : Type u_5) [Semiring R] {α' : Type u_7} {M' : Type u_8} [AddCommMonoid M'] [Module R M'] {v' : α' → M'} (f : α → α') (l : α →₀ R) :

(Finsupp.linearCombination R v') (Finsupp.mapDomain f l) = (Finsupp.linearCombination R (v' ∘ f)) l

source

@[deprecated Finsupp.linearCombination_mapDomain (since := "2024-08-29")]

theorem Finsupp.total_mapDomain {α : Type u_1} (R : Type u_5) [Semiring R] {α' : Type u_7} {M' : Type u_8} [AddCommMonoid M'] [Module R M'] {v' : α' → M'} (f : α → α') (l : α →₀ R) :

(Finsupp.linearCombination R v') (Finsupp.mapDomain f l) = (Finsupp.linearCombination R (v' ∘ f)) l

Alias of Finsupp.linearCombination_mapDomain.

source

@[simp]

theorem Finsupp.linearCombination_equivMapDomain {α : Type u_1} (R : Type u_5) [Semiring R] {α' : Type u_7} {M' : Type u_8} [AddCommMonoid M'] [Module R M'] {v' : α' → M'} (f : α ≃ α') (l : α →₀ R) :

(Finsupp.linearCombination R v') (Finsupp.equivMapDomain f l) = (Finsupp.linearCombination R (v' ∘ ⇑f)) l

source

@[deprecated Finsupp.linearCombination_equivMapDomain (since := "2024-08-29")]

theorem Finsupp.total_equivMapDomain {α : Type u_1} (R : Type u_5) [Semiring R] {α' : Type u_7} {M' : Type u_8} [AddCommMonoid M'] [Module R M'] {v' : α' → M'} (f : α ≃ α') (l : α →₀ R) :

(Finsupp.linearCombination R v') (Finsupp.equivMapDomain f l) = (Finsupp.linearCombination R (v' ∘ ⇑f)) l

Alias of Finsupp.linearCombination_equivMapDomain.

source

theorem Finsupp.span_eq_range_linearCombination {M : Type u_2} (R : Type u_5) [Semiring R] [AddCommMonoid M] [Module R M] (s : Set M) :

Submodule.span R s = LinearMap.range (Finsupp.linearCombination R Subtype.val)

A version of Finsupp.range_linearCombination which is useful for going in the other direction

source

@[deprecated Finsupp.span_eq_range_linearCombination (since := "2024-08-29")]

theorem Finsupp.span_eq_range_total {M : Type u_2} (R : Type u_5) [Semiring R] [AddCommMonoid M] [Module R M] (s : Set M) :

Submodule.span R s = LinearMap.range (Finsupp.linearCombination R Subtype.val)

Alias of Finsupp.span_eq_range_linearCombination.

A version of Finsupp.range_linearCombination which is useful for going in the other direction

source

theorem Finsupp.mem_span_iff_linearCombination {M : Type u_2} (R : Type u_5) [Semiring R] [AddCommMonoid M] [Module R M] (s : Set M) (x : M) :

x ∈ Submodule.span R s ↔ ∃ (l : ↑s →₀ R), (Finsupp.linearCombination R Subtype.val) l = x

source

@[deprecated Finsupp.mem_span_iff_linearCombination (since := "2024-08-29")]

theorem Finsupp.mem_span_iff_total {M : Type u_2} (R : Type u_5) [Semiring R] [AddCommMonoid M] [Module R M] (s : Set M) (x : M) :

x ∈ Submodule.span R s ↔ ∃ (l : ↑s →₀ R), (Finsupp.linearCombination R Subtype.val) l = x

Alias of Finsupp.mem_span_iff_linearCombination.

source

theorem Finsupp.mem_span_range_iff_exists_finsupp {α : Type u_1} {M : Type u_2} {R : Type u_5} [Semiring R] [AddCommMonoid M] [Module R M] {v : α → M} {x : M} :

x ∈ Submodule.span R (Set.range v) ↔ ∃ (c : α →₀ R), (c.sum fun (i : α) (a : R) => a • v i) = x

source

theorem Finsupp.span_image_eq_map_linearCombination {α : Type u_1} {M : Type u_2} (R : Type u_5) [Semiring R] [AddCommMonoid M] [Module R M] {v : α → M} (s : Set α) :

Submodule.span R (v '' s) = Submodule.map (Finsupp.linearCombination R v) (Finsupp.supported R R s)

source

@[deprecated Finsupp.span_image_eq_map_linearCombination (since := "2024-08-29")]

theorem Finsupp.span_image_eq_map_total {α : Type u_1} {M : Type u_2} (R : Type u_5) [Semiring R] [AddCommMonoid M] [Module R M] {v : α → M} (s : Set α) :

Submodule.span R (v '' s) = Submodule.map (Finsupp.linearCombination R v) (Finsupp.supported R R s)

Alias of Finsupp.span_image_eq_map_linearCombination.

source

theorem Finsupp.mem_span_image_iff_linearCombination {α : Type u_1} {M : Type u_2} (R : Type u_5) [Semiring R] [AddCommMonoid M] [Module R M] {v : α → M} {s : Set α} {x : M} :

x ∈ Submodule.span R (v '' s) ↔ ∃ l ∈ Finsupp.supported R R s, (Finsupp.linearCombination R v) l = x

source

@[deprecated Finsupp.mem_span_image_iff_linearCombination (since := "2024-08-29")]

theorem Finsupp.mem_span_image_iff_total {α : Type u_1} {M : Type u_2} (R : Type u_5) [Semiring R] [AddCommMonoid M] [Module R M] {v : α → M} {s : Set α} {x : M} :

x ∈ Submodule.span R (v '' s) ↔ ∃ l ∈ Finsupp.supported R R s, (Finsupp.linearCombination R v) l = x

Alias of Finsupp.mem_span_image_iff_linearCombination.

source

theorem Finsupp.linearCombination_option {α : Type u_1} {M : Type u_2} (R : Type u_5) [Semiring R] [AddCommMonoid M] [Module R M] (v : Option α → M) (f : Option α →₀ R) :

(Finsupp.linearCombination R v) f = f none • v none + (Finsupp.linearCombination R (v ∘ some)) f.some

source

@[deprecated Finsupp.linearCombination_option (since := "2024-08-29")]

theorem Finsupp.total_option {α : Type u_1} {M : Type u_2} (R : Type u_5) [Semiring R] [AddCommMonoid M] [Module R M] (v : Option α → M) (f : Option α →₀ R) :

(Finsupp.linearCombination R v) f = f none • v none + (Finsupp.linearCombination R (v ∘ some)) f.some

Alias of Finsupp.linearCombination_option.

source

theorem Finsupp.linearCombination_linearCombination {M : Type u_2} (R : Type u_5) [Semiring R] [AddCommMonoid M] [Module R M] {α : Type u_9} {β : Type u_10} (A : α → M) (B : β → α →₀ R) (f : β →₀ R) :

(Finsupp.linearCombination R A) ((Finsupp.linearCombination R B) f) = (Finsupp.linearCombination R fun (b : β) => (Finsupp.linearCombination R A) (B b)) f

source

@[deprecated Finsupp.linearCombination_linearCombination (since := "2024-08-29")]

theorem Finsupp.total_total {M : Type u_2} (R : Type u_5) [Semiring R] [AddCommMonoid M] [Module R M] {α : Type u_9} {β : Type u_10} (A : α → M) (B : β → α →₀ R) (f : β →₀ R) :

(Finsupp.linearCombination R A) ((Finsupp.linearCombination R B) f) = (Finsupp.linearCombination R fun (b : β) => (Finsupp.linearCombination R A) (B b)) f

Alias of Finsupp.linearCombination_linearCombination.

source

theorem Finsupp.linearCombination_smul {α : Type u_1} {M : Type u_2} (R : Type u_5) {S : Type u_6} [Semiring R] [Semiring S] [AddCommMonoid M] [Module R M] {α' : Type u_7} {v : α → M} [Module R S] [Module S M] [IsScalarTower R S M] {w : α' → S} :

(Finsupp.linearCombination R fun (i : α × α') => w i.2 • v i.1) = ↑R (Finsupp.linearCombination S v) ∘ₗ Finsupp.mapRange.linearMap (Finsupp.linearCombination R w) ∘ₗ ↑(Finsupp.finsuppProdLEquiv R)

source

@[simp]

theorem Finsupp.linearCombination_fin_zero {M : Type u_2} (R : Type u_5) [Semiring R] [AddCommMonoid M] [Module R M] (f : Fin 0 → M) :

Finsupp.linearCombination R f = 0

source

@[deprecated Finsupp.linearCombination_fin_zero (since := "2024-08-29")]

theorem Finsupp.total_fin_zero {M : Type u_2} (R : Type u_5) [Semiring R] [AddCommMonoid M] [Module R M] (f : Fin 0 → M) :

Finsupp.linearCombination R f = 0

Alias of Finsupp.linearCombination_fin_zero.

source

def Finsupp.linearCombinationOn (α : Type u_1) (M : Type u_2) (R : Type u_5) [Semiring R] [AddCommMonoid M] [Module R M] (v : α → M) (s : Set α) :

↥(Finsupp.supported R R s) →ₗ[R] ↥(Submodule.span R (v '' s))

Finsupp.linearCombinationOn M v s interprets p : α →₀ R as a linear combination of a subset of the vectors in v, mapping it to the span of those vectors.

The subset is indicated by a set s : Set α of indices.

Equations

Finsupp.linearCombinationOn α M R v s = LinearMap.codRestrict (Submodule.span R (v '' s)) (Finsupp.linearCombination R v ∘ₗ (Finsupp.supported R R s).subtype) ⋯

Instances For

source

@[deprecated Finsupp.linearCombinationOn (since := "2024-08-29")]

def Finsupp.totalOn (α : Type u_1) (M : Type u_2) (R : Type u_5) [Semiring R] [AddCommMonoid M] [Module R M] (v : α → M) (s : Set α) :

↥(Finsupp.supported R R s) →ₗ[R] ↥(Submodule.span R (v '' s))

Alias of Finsupp.linearCombinationOn.

Finsupp.linearCombinationOn M v s interprets p : α →₀ R as a linear combination of a subset of the vectors in v, mapping it to the span of those vectors.

The subset is indicated by a set s : Set α of indices.

Equations

Finsupp.totalOn = Finsupp.linearCombinationOn

Instances For

source

theorem Finsupp.linearCombinationOn_range {α : Type u_1} {M : Type u_2} (R : Type u_5) [Semiring R] [AddCommMonoid M] [Module R M] {v : α → M} (s : Set α) :

LinearMap.range (Finsupp.linearCombinationOn α M R v s) = ⊤

source

@[deprecated Finsupp.linearCombinationOn_range (since := "2024-08-29")]

theorem Finsupp.totalOn_range {α : Type u_1} {M : Type u_2} (R : Type u_5) [Semiring R] [AddCommMonoid M] [Module R M] {v : α → M} (s : Set α) :

LinearMap.range (Finsupp.linearCombinationOn α M R v s) = ⊤

Alias of Finsupp.linearCombinationOn_range.

source

theorem Finsupp.linearCombination_restrict {α : Type u_1} {M : Type u_2} (R : Type u_5) [Semiring R] [AddCommMonoid M] [Module R M] {v : α → M} (s : Set α) :

Finsupp.linearCombination R (s.restrict v) = (Submodule.span R (v '' s)).subtype ∘ₗ Finsupp.linearCombinationOn α M R v s ∘ₗ ↑(Finsupp.supportedEquivFinsupp s).symm

source

theorem Finsupp.linearCombination_comp {α : Type u_1} {M : Type u_2} (R : Type u_5) [Semiring R] [AddCommMonoid M] [Module R M] {α' : Type u_7} {v : α → M} (f : α' → α) :

Finsupp.linearCombination R (v ∘ f) = Finsupp.linearCombination R v ∘ₗ Finsupp.lmapDomain R R f

source

@[deprecated Finsupp.linearCombination_comp (since := "2024-08-29")]

theorem Finsupp.total_comp {α : Type u_1} {M : Type u_2} (R : Type u_5) [Semiring R] [AddCommMonoid M] [Module R M] {α' : Type u_7} {v : α → M} (f : α' → α) :

Finsupp.linearCombination R (v ∘ f) = Finsupp.linearCombination R v ∘ₗ Finsupp.lmapDomain R R f

Alias of Finsupp.linearCombination_comp.

source

theorem Finsupp.linearCombination_comapDomain {α : Type u_1} {M : Type u_2} (R : Type u_5) [Semiring R] [AddCommMonoid M] [Module R M] {α' : Type u_7} {v : α → M} (f : α → α') (l : α' →₀ R) (hf : Set.InjOn f (f ⁻¹' ↑l.support)) :

(Finsupp.linearCombination R v) (Finsupp.comapDomain f l hf) = ∑ i ∈ l.support.preimage f hf, l (f i) • v i

source

@[deprecated Finsupp.linearCombination_comapDomain (since := "2024-08-29")]

theorem Finsupp.total_comapDomain {α : Type u_1} {M : Type u_2} (R : Type u_5) [Semiring R] [AddCommMonoid M] [Module R M] {α' : Type u_7} {v : α → M} (f : α → α') (l : α' →₀ R) (hf : Set.InjOn f (f ⁻¹' ↑l.support)) :

(Finsupp.linearCombination R v) (Finsupp.comapDomain f l hf) = ∑ i ∈ l.support.preimage f hf, l (f i) • v i

Alias of Finsupp.linearCombination_comapDomain.

source

theorem Finsupp.linearCombination_onFinset {α : Type u_1} {M : Type u_2} (R : Type u_5) [Semiring R] [AddCommMonoid M] [Module R M] {s : Finset α} {f : α → R} (g : α → M) (hf : ∀ (a : α), f a ≠ 0 → a ∈ s) :

(Finsupp.linearCombination R g) (Finsupp.onFinset s f hf) = ∑ x ∈ s, f x • g x

source

@[deprecated Finsupp.linearCombination_onFinset (since := "2024-08-29")]

theorem Finsupp.total_onFinset {α : Type u_1} {M : Type u_2} (R : Type u_5) [Semiring R] [AddCommMonoid M] [Module R M] {s : Finset α} {f : α → R} (g : α → M) (hf : ∀ (a : α), f a ≠ 0 → a ∈ s) :

(Finsupp.linearCombination R g) (Finsupp.onFinset s f hf) = ∑ x ∈ s, f x • g x

Alias of Finsupp.linearCombination_onFinset.

source

def Fintype.linearCombination {α : Type u_1} {M : Type u_2} (R : Type u_3) [Fintype α] [Semiring R] [AddCommMonoid M] [Module R M] (S : Type u_4) [Semiring S] [Module S M] [SMulCommClass R S M] :

(α → M) →ₗ[S] (α → R) →ₗ[R] M

Fintype.linearCombination R S v f is the linear combination of vectors in v with weights in f. This variant of Finsupp.linearCombination is defined on fintype indexed vectors.

This map is linear in v if R is commutative, and always linear in f. See note [bundled maps over different rings] for why separate R and S semirings are used.

Equations

Fintype.linearCombination R S = { toFun := fun (v : α → M) => { toFun := fun (f : α → R) => ∑ i : α, f i • v i, map_add' := ⋯, map_smul' := ⋯ }, map_add' := ⋯, map_smul' := ⋯ }

Instances For

source

@[deprecated Fintype.linearCombination (since := "2024-08-29")]

def Fintype.total {α : Type u_1} {M : Type u_2} (R : Type u_3) [Fintype α] [Semiring R] [AddCommMonoid M] [Module R M] (S : Type u_4) [Semiring S] [Module S M] [SMulCommClass R S M] :

(α → M) →ₗ[S] (α → R) →ₗ[R] M

Alias of Fintype.linearCombination.

Fintype.linearCombination R S v f is the linear combination of vectors in v with weights in f. This variant of Finsupp.linearCombination is defined on fintype indexed vectors.

This map is linear in v if R is commutative, and always linear in f. See note [bundled maps over different rings] for why separate R and S semirings are used.

Equations

@Fintype.total = @Fintype.linearCombination

Instances For

source

theorem Fintype.linearCombination_apply {α : Type u_1} {M : Type u_2} (R : Type u_3) [Fintype α] [Semiring R] [AddCommMonoid M] [Module R M] {S : Type u_4} [Semiring S] [Module S M] [SMulCommClass R S M] (v : α → M) (f : α → R) :

((Fintype.linearCombination R S) v) f = ∑ i : α, f i • v i

source

@[deprecated Fintype.linearCombination_apply (since := "2024-08-29")]

theorem Fintype.total_apply {α : Type u_1} {M : Type u_2} (R : Type u_3) [Fintype α] [Semiring R] [AddCommMonoid M] [Module R M] {S : Type u_4} [Semiring S] [Module S M] [SMulCommClass R S M] (v : α → M) (f : α → R) :

((Fintype.linearCombination R S) v) f = ∑ i : α, f i • v i

Alias of Fintype.linearCombination_apply.

source

@[simp]

theorem Fintype.linearCombination_apply_single {α : Type u_1} {M : Type u_2} (R : Type u_3) [Fintype α] [Semiring R] [AddCommMonoid M] [Module R M] {S : Type u_4} [Semiring S] [Module S M] [SMulCommClass R S M] (v : α → M) [DecidableEq α] (i : α) (r : R) :

((Fintype.linearCombination R S) v) (Pi.single i r) = r • v i

source

@[deprecated Fintype.linearCombination_apply_single (since := "2024-08-29")]

theorem Fintype.total_apply_single {α : Type u_1} {M : Type u_2} (R : Type u_3) [Fintype α] [Semiring R] [AddCommMonoid M] [Module R M] {S : Type u_4} [Semiring S] [Module S M] [SMulCommClass R S M] (v : α → M) [DecidableEq α] (i : α) (r : R) :

((Fintype.linearCombination R S) v) (Pi.single i r) = r • v i

Alias of Fintype.linearCombination_apply_single.

source

theorem Finsupp.linearCombination_eq_fintype_linearCombination_apply {α : Type u_1} {M : Type u_2} (R : Type u_3) [Fintype α] [Semiring R] [AddCommMonoid M] [Module R M] (S : Type u_4) [Semiring S] [Module S M] [SMulCommClass R S M] (v : α → M) (x : α → R) :

(Finsupp.linearCombination R v) ((Finsupp.linearEquivFunOnFinite R R α).symm x) = ((Fintype.linearCombination R S) v) x

source

@[deprecated Finsupp.linearCombination_eq_fintype_linearCombination_apply (since := "2024-08-29")]

theorem Finsupp.total_eq_fintype_total_apply {α : Type u_1} {M : Type u_2} (R : Type u_3) [Fintype α] [Semiring R] [AddCommMonoid M] [Module R M] (S : Type u_4) [Semiring S] [Module S M] [SMulCommClass R S M] (v : α → M) (x : α → R) :

(Finsupp.linearCombination R v) ((Finsupp.linearEquivFunOnFinite R R α).symm x) = ((Fintype.linearCombination R S) v) x

Alias of Finsupp.linearCombination_eq_fintype_linearCombination_apply.

source

theorem Finsupp.linearCombination_eq_fintype_linearCombination {α : Type u_1} {M : Type u_2} (R : Type u_3) [Fintype α] [Semiring R] [AddCommMonoid M] [Module R M] (S : Type u_4) [Semiring S] [Module S M] [SMulCommClass R S M] (v : α → M) :

Finsupp.linearCombination R v ∘ₗ ↑(Finsupp.linearEquivFunOnFinite R R α).symm = (Fintype.linearCombination R S) v

source

@[deprecated Finsupp.linearCombination_eq_fintype_linearCombination (since := "2024-08-29")]

theorem Finsupp.total_eq_fintype_total {α : Type u_1} {M : Type u_2} (R : Type u_3) [Fintype α] [Semiring R] [AddCommMonoid M] [Module R M] (S : Type u_4) [Semiring S] [Module S M] [SMulCommClass R S M] (v : α → M) :

Finsupp.linearCombination R v ∘ₗ ↑(Finsupp.linearEquivFunOnFinite R R α).symm = (Fintype.linearCombination R S) v

Alias of Finsupp.linearCombination_eq_fintype_linearCombination.

source

@[simp]

theorem Fintype.range_linearCombination {α : Type u_1} {M : Type u_2} (R : Type u_3) [Fintype α] [Semiring R] [AddCommMonoid M] [Module R M] {S : Type u_4} [Semiring S] [Module S M] [SMulCommClass R S M] (v : α → M) :

LinearMap.range ((Fintype.linearCombination R S) v) = Submodule.span R (Set.range v)

source

@[deprecated Fintype.range_linearCombination (since := "2024-08-29")]

theorem Fintype.range_total {α : Type u_1} {M : Type u_2} (R : Type u_3) [Fintype α] [Semiring R] [AddCommMonoid M] [Module R M] {S : Type u_4} [Semiring S] [Module S M] [SMulCommClass R S M] (v : α → M) :

LinearMap.range ((Fintype.linearCombination R S) v) = Submodule.span R (Set.range v)

Alias of Fintype.range_linearCombination.

source

theorem mem_span_range_iff_exists_fun {α : Type u_1} {M : Type u_2} (R : Type u_3) [Fintype α] [Semiring R] [AddCommMonoid M] [Module R M] {v : α → M} {x : M} :

x ∈ Submodule.span R (Set.range v) ↔ ∃ (c : α → R), ∑ i : α, c i • v i = x

An element x lies in the span of v iff it can be written as sum ∑ cᵢ • vᵢ = x.

source

theorem top_le_span_range_iff_forall_exists_fun {α : Type u_1} {M : Type u_2} (R : Type u_3) [Fintype α] [Semiring R] [AddCommMonoid M] [Module R M] {v : α → M} :

⊤ ≤ Submodule.span R (Set.range v) ↔ ∀ (x : M), ∃ (c : α → R), ∑ i : α, c i • v i = x

A family v : α → V is generating V iff every element (x : V) can be written as sum ∑ cᵢ • vᵢ = x.

source

theorem Span.repr_def (R : Type u_4) {M : Type u_5} [Semiring R] [AddCommMonoid M] [Module R M] (w : Set M) (x : ↥(Submodule.span R w)) :

Span.repr R w x = ⋯.choose

source

@[irreducible]

def Span.repr (R : Type u_4) {M : Type u_5} [Semiring R] [AddCommMonoid M] [Module R M] (w : Set M) (x : ↥(Submodule.span R w)) :

↑w →₀ R

Pick some representation of x : span R w as a linear combination in w, ((Finsupp.mem_span_iff_linearCombination _ _ _).mp x.2).choose

Equations

Span.repr R w x = ⋯.choose

Instances For

source

@[simp]

theorem Span.finsupp_linearCombination_repr (R : Type u_1) {M : Type u_2} [Semiring R] [AddCommMonoid M] [Module R M] {w : Set M} (x : ↥(Submodule.span R w)) :

(Finsupp.linearCombination R Subtype.val) (Span.repr R w x) = ↑x

source

@[deprecated Span.finsupp_linearCombination_repr (since := "2024-08-29")]

theorem Span.finsupp_total_repr (R : Type u_1) {M : Type u_2} [Semiring R] [AddCommMonoid M] [Module R M] {w : Set M} (x : ↥(Submodule.span R w)) :

(Finsupp.linearCombination R Subtype.val) (Span.repr R w x) = ↑x

Alias of Span.finsupp_linearCombination_repr.

source

theorem LinearMap.map_finsupp_linearCombination {R : Type u_1} {M : Type u_2} {N : Type u_3} [Semiring R] [AddCommMonoid M] [Module R M] [AddCommMonoid N] [Module R N] (f : M →ₗ[R] N) {ι : Type u_4} {g : ι → M} (l : ι →₀ R) :

f ((Finsupp.linearCombination R g) l) = (Finsupp.linearCombination R (⇑f ∘ g)) l

source

@[deprecated LinearMap.map_finsupp_linearCombination (since := "2024-08-29")]

theorem LinearMap.map_finsupp_total {R : Type u_1} {M : Type u_2} {N : Type u_3} [Semiring R] [AddCommMonoid M] [Module R M] [AddCommMonoid N] [Module R N] (f : M →ₗ[R] N) {ι : Type u_4} {g : ι → M} (l : ι →₀ R) :

f ((Finsupp.linearCombination R g) l) = (Finsupp.linearCombination R (⇑f ∘ g)) l

Alias of LinearMap.map_finsupp_linearCombination.

source

theorem mem_span_finset {R : Type u_1} {M : Type u_2} [Semiring R] [AddCommMonoid M] [Module R M] {s : Finset M} {x : M} :

x ∈ Submodule.span R ↑s ↔ ∃ (f : M → R), ∑ i ∈ s, f i • i = x

source

theorem mem_span_set {R : Type u_1} {M : Type u_2} [Semiring R] [AddCommMonoid M] [Module R M] {m : M} {s : Set M} :

m ∈ Submodule.span R s ↔ ∃ (c : M →₀ R), ↑c.support ⊆ s ∧ (c.sum fun (mi : M) (r : R) => r • mi) = m

An element m ∈ M is contained in the R-submodule spanned by a set s ⊆ M, if and only if m can be written as a finite R-linear combination of elements of s. The implementation uses Finsupp.sum.

source

theorem mem_span_set' {R : Type u_1} {M : Type u_2} [Semiring R] [AddCommMonoid M] [Module R M] {m : M} {s : Set M} :

m ∈ Submodule.span R s ↔ ∃ (n : ℕ) (f : Fin n → R) (g : Fin n → ↑s), ∑ i : Fin n, f i • ↑(g i) = m

source

theorem span_eq_iUnion_nat {R : Type u_1} {M : Type u_2} [Semiring R] [AddCommMonoid M] [Module R M] (s : Set M) :

↑(Submodule.span R s) = ⋃ (n : ℕ), (fun (f : Fin n → R × M) => ∑ i : Fin n, (f i).1 • (f i).2) '' {f : Fin n → R × M | ∀ (i : Fin n), (f i).2 ∈ s}

The span of a subset s is the union over all n of the set of linear combinations of at most n terms belonging to s.

Documentation

Mathlib.LinearAlgebra.Finsupp.LinearCombination

`Finsupp.linearCombination` #

Main definitions #

Tags #

Finsupp.linearCombination #

Main definitions #

Tags #

`Finsupp.linearCombination` #