Theorems · Theorem · linear algebra

Finsupp.linearCombination_embDomain

∀ {α : Type u_1} (R : Type u_5) [inst : Semiring R] {α' : Type u_7} {M' : Type u_8} [inst_1 : AddCommMonoid M']
  [inst_2 : Module R M'] {v' : α' → M'} (f : α ↪ α') (l : α →₀ R),
  (Finsupp.linearCombination R v') (Finsupp.embDomain f l) = (Finsupp.linearCombination R (v' ∘ ⇑f)) l

Defined in

Mathlib.LinearAlgebra.Finsupp.LinearCombination

Cited by

0 results in Mathlib

Foundations

Depth 78 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

SemiringAddCommMonoidModule