Theorems · Definition · linear algebra

Finsupp.linearCombination

{α : Type u_1} →
  {M : Type u_2} →
    (R : Type u_5) →
      [inst : Semiring R] → [inst_1 : AddCommMonoid M] → [inst_2 : Module R M] → (α → M) → (α →₀ R) →ₗ[R] M

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

Defined in

Mathlib.LinearAlgebra.Finsupp.LinearCombination

Cited by

269 results in Mathlib

Foundations

Depth 77 from the axioms, rests on 1,816 definitions · uses propext, Classical.choice, Quot.sound

Assumes

SemiringAddCommMonoidModule