Theorems · Definition · linear algebra

PiTensorProduct.tprodCoeff

{ι : Type u_1} →
  (R : Type u_4) →
    [inst : CommSemiring R] →
      {s : ι → Type u_7} →
        [inst_1 : (i : ι) → AddCommMonoid (s i)] →
          [inst_2 : (i : ι) → Module R (s i)] → R → ((i : ι) → s i) → PiTensorProduct R fun i => s i

tprodCoeff R r f with r : R and f : Π i, s i is the tensor product of the vectors f i over all i : ι, multiplied by the coefficient r. Note that this is meant as an auxiliary definition for this file alone, and that one should use tprod defined below for most purposes.

Defined in

Mathlib.LinearAlgebra.PiTensorProduct.Basic

Cited by

13 results in Mathlib

Foundations

Depth 40 from the axioms · uses propext, Quot.sound

Assumes

CommSemiringAddCommMonoidModule