# `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

- `Fintype.linearCombination R (v : ι → M)`: sends `l : ι → R` to the linear combination of `v i` with coefficients `l i` (for a finite type `ι`)

- `Finsupp.bilinearCombination R S`, `Fintype.bilinearCombination R S`: a bilinear version of `Finsupp.linearCombination` and `Fintype.linearCombination`. It requires that `M` is both an `R`-module and an `S`-module, with `SMulCommClass R S M`; the case `S = R` typically requires that `R` is commutative.

## Tags #

function with finite support, module, linear algebra

source
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
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) :
(linearCombination R v) l = l.sum fun (i : α) (a : R) => a • v i
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 ∈ supported R R ↑s) :
(linearCombination R v) l = ∑ i ∈ s, l i • v i
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 : α) :
(linearCombination R v) (single a c) = c • v a
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) :
(linearCombination R 0) x = 0
source
@[simp]
theorem Finsupp.linearCombination_zero (α : Type u_1) (M : Type u_2) (R : Type u_5) [Semiring R] [AddCommMonoid M] [Module R M] :
linearCombination R 0 = 0
source
@[simp]
theorem Finsupp.linearCombination_single_index (α : Type u_1) (M : Type u_2) (R : Type u_5) [Semiring R] [AddCommMonoid M] [Module R M] (c : M) (a : α) (f : α →₀ R) [DecidableEq α] :
(linearCombination R (Pi.single a c)) f = f a • c
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') :
linearCombination R (⇑f ∘ v) = f ∘ₗ 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 ((linearCombination R v) l) = (linearCombination R (⇑f ∘ v)) l
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 ((linearCombination R id) l) = (linearCombination R ⇑f) l
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) :
(linearCombination R v) l = l default • v default
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 ⇑(linearCombination R v)
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 (linearCombination R v) = ⊤
source
theorem Finsupp.linearCombination_id_surjective (R : Type u_5) [Semiring R] (M : Type u_9) [AddCommMonoid M] [Module R M] :
Function.Surjective ⇑(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
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 (linearCombination R v) = Submodule.span R (Set.range v)
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)) :
linearCombination R v' ∘ₗ lmapDomain R R f = g ∘ₗ linearCombination R v
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 : α → α') :
linearCombination R v' ∘ₗ lmapDomain R R f = linearCombination R (v' ∘ f)
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) :
(linearCombination R v') (embDomain f l) = (linearCombination R (v' ∘ ⇑f)) l
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) :
(linearCombination R v') (mapDomain f l) = (linearCombination R (v' ∘ f)) l
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) :
(linearCombination R v') (equivMapDomain f l) = (linearCombination R (v' ∘ ⇑f)) l
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 (linearCombination R Subtype.val)

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), (linearCombination R Subtype.val) l = x
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 (linearCombination R v) (supported R R s)
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 ∈ supported R R s, (linearCombination R v) l = x
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) :
(linearCombination R v) f = f none • v none + (linearCombination R (v ∘ Option.some)) f.some
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) :
(linearCombination R A) ((linearCombination R B) f) = (linearCombination R fun (b : β) => (linearCombination R A) (B b)) f
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} [DecidableEq α] [Module R S] [Module S M] [IsScalarTower R S M] {w : α' → S} :
(linearCombination R fun (i : α × α') => w i.2 • v i.1) = ↑R (linearCombination S v) ∘ₗ mapRange.linearMap (linearCombination R w) ∘ₗ ↑(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) :
linearCombination R f = 0
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 α) :
↥(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
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 (linearCombinationOn α M R v s) = ⊤
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 α) :
linearCombination R (s.restrict v) = (Submodule.span R (v '' s)).subtype ∘ₗ linearCombinationOn α M R v s ∘ₗ ↑(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 : α' → α) :
linearCombination R (v ∘ f) = linearCombination R v ∘ₗ lmapDomain R R f
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)) :
(linearCombination R v) (comapDomain f l hf) = ∑ i ∈ l.support.preimage f hf, l (f i) • v i
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) :
(linearCombination R g) (onFinset s f hf) = ∑ x ∈ s, f x • g x
source
def Finsupp.bilinearCombination {α : Type u_1} {M : Type u_2} (R : Type u_5) (S : Type u_6) [Semiring R] [Semiring S] [AddCommMonoid M] [Module R M] [Module S M] [SMulCommClass R S M] :
(α → M) →ₗ[S] (α →₀ R) →ₗ[R] M

`Finsupp.bilinearCombination R S v f` is the linear combination of vectors in `v` with weights in `f`, as a bilinear map of `v` and `f`. In the absence of `SMulCommClass R S M`, use `Finsupp.linearCombination`.

See note [bundled maps over different rings] for why separate `R` and `S` semirings are used.

Equations

- Finsupp.bilinearCombination R S = { toFun := fun (v : α → M) => Finsupp.linearCombination R v, map_add' := ⋯, map_smul' := ⋯ }

Instances For

source
@[simp]
theorem Finsupp.bilinearCombination_apply {α : Type u_1} {M : Type u_2} (R : Type u_5) {S : Type u_6} [Semiring R] [Semiring S] [AddCommMonoid M] [Module R M] {v : α → M} [Module S M] [SMulCommClass R S M] :
(bilinearCombination R S) v = linearCombination R v
source
def Fintype.linearCombination {α : Type u_1} {M : Type u_2} (R : Type u_3) [Fintype α] [Semiring R] [AddCommMonoid M] [Module R M] (v : α → M) :
(α → R) →ₗ[R] M

`Fintype.linearCombination R 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 v = { toFun := fun (f : α → R) => ∑ i : α, f i • v i, map_add' := ⋯, map_smul' := ⋯ }

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] (v : α → M) (f : α → R) :
(Fintype.linearCombination R v) f = ∑ i : α, f i • v i
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] (v : α → M) [DecidableEq α] (i : α) (r : R) :
(Fintype.linearCombination R v) (Pi.single i r) = r • v i
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] (v : α → M) (x : α → R) :
(linearCombination R v) ((linearEquivFunOnFinite R R α).symm x) = (Fintype.linearCombination R v) x
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] (v : α → M) :
linearCombination R v ∘ₗ ↑(linearEquivFunOnFinite R R α).symm = Fintype.linearCombination R v
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] (v : α → M) :
LinearMap.range (Fintype.linearCombination R v) = Submodule.span R (Set.range v)
source
def Fintype.bilinearCombination {α : 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.bilinearCombination 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.bilinearCombination R S = { toFun := fun (v : α → M) => Fintype.linearCombination R v, map_add' := ⋯, map_smul' := ⋯ }

Instances For

source
@[simp]
theorem Fintype.bilinearCombination_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) :
(Fintype.bilinearCombination R S) v = Fintype.linearCombination R v
source
theorem Fintype.bilinearCombination_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.bilinearCombination R S) v) (Pi.single i r) = r • v i
source
theorem Submodule.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 ∈ 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 Submodule.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} :
⊤ ≤ 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 Submodule.mem_span_image_iff_exists_fun {α : Type u_1} {M : Type u_2} (R : Type u_3) [Semiring R] [AddCommMonoid M] [Module R M] {v : α → M} {x : M} {s : Set α} :
x ∈ span R (v '' s) ↔ ∃ (t : Finset α), ↑t ⊆ s ∧ ∃ (c : ↥t → R), ∑ i : ↥t, c i • v ↑i = x
source
theorem Fintype.mem_span_image_iff_exists_fun {α : Type u_1} {M : Type u_2} (R : Type u_3) [Semiring R] [AddCommMonoid M] [Module R M] {v : α → M} {x : M} {s : Set α} [Fintype ↑s] :
x ∈ Submodule.span R (v '' s) ↔ ∃ (c : ↑s → R), ∑ i : ↑s, c i • v ↑i = x
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
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)) :
repr R w x = ⋯.choose
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) (repr R w x) = ↑x
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
theorem Submodule.mem_span_iff_exists_finset_subset {R : Type u_1} {M : Type u_2} [Semiring R] [AddCommMonoid M] [Module R M] {s : Set M} {x : M} :
x ∈ span R s ↔ ∃ (f : M → R) (t : Finset M), ↑t ⊆ s ∧ Function.support f ⊆ ↑t ∧ ∑ a ∈ t, f a • a = x
source
theorem Submodule.mem_span_finset {R : Type u_1} {M : Type u_2} [Semiring R] [AddCommMonoid M] [Module R M] {s : Finset M} {x : M} :
x ∈ span R ↑s ↔ ∃ (f : M → R), Function.support f ⊆ ↑s ∧ ∑ a ∈ s, f a • a = x
source
theorem Submodule.mem_span_iff_of_fintype {R : Type u_1} {M : Type u_2} [Semiring R] [AddCommMonoid M] [Module R M] {s : Set M} [Fintype ↑s] {x : M} :
x ∈ span R s ↔ ∃ (f : ↑s → R), ∑ a : ↑s, f a • ↑a = x
source
theorem Submodule.mem_span_finset' {R : Type u_1} {M : Type u_2} [Semiring R] [AddCommMonoid M] [Module R M] {s : Finset M} {x : M} :
x ∈ span R ↑s ↔ ∃ (f : ↥s → R), ∑ a : ↥s, f a • ↑a = x

A variant of `Submodule.mem_span_finset` using `s` as the index type.

source
theorem Submodule.mem_span_set {R : Type u_1} {M : Type u_2} [Semiring R] [AddCommMonoid M] [Module R M] {m : M} {s : Set M} :
m ∈ 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 Submodule.mem_span_set' {R : Type u_1} {M : Type u_2} [Semiring R] [AddCommMonoid M] [Module R M] {m : M} {s : Set M} :
m ∈ span R s ↔ ∃ (n : ℕ) (f : Fin n → R) (g : Fin n → ↑s), ∑ i : Fin n, f i • ↑(g i) = 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 a sum indexed by `Fin n` for some `n`.

source
theorem Submodule.span_eq_iUnion_nat {R : Type u_1} {M : Type u_2} [Semiring R] [AddCommMonoid M] [Module R M] (s : Set M) :
↑(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`.

source
def Finsupp.addSingleEquiv {R : Type u_4} {ι : Type u_6} [Ring R] (i : ι) (c : ι → R) (h₀ : c i = 0) :
(ι →₀ R) ≃ₗ[R] ι →₀ R

Given `c : ι → R` and an index `i` such that `c i = 0`, this is the linear isomorphism sending the `j`-th standard basis vector to itself plus `c j` multiplied with the `i`-th standard basis vector (in particular, the `i`-th standard basis vector is kept invariant).

Equations

- One or more equations did not get rendered due to their size.

Instances For

source
theorem Finsupp.linearCombination_comp_addSingleEquiv {R : Type u_4} {M : Type u_5} {ι : Type u_6} [Ring R] [AddCommGroup M] [Module R M] (i : ι) (c : ι → R) (h₀ : c i = 0) (v : ι → M) :
linearCombination R v ∘ₗ ↑(addSingleEquiv i c h₀) = linearCombination R (v + fun (x : ι) => c x • v i)