Theorems · Definition · linear algebra

PiTensorProduct.mapMultilinear

{ι : 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)] →
            (t : ι → Type u_11) →
              [inst_3 : (i : ι) → AddCommMonoid (t i)] →
                [inst_4 : (i : ι) → Module R (t i)] →
                  MultilinearMap R (fun i => s i →ₗ[R] t i)
                    ((PiTensorProduct R fun i => s i) →ₗ[R] PiTensorProduct R fun i => t i)

The tensor of a family of linear maps from sᵢ to tᵢ, as a multilinear map of the family.

Defined in

Mathlib.LinearAlgebra.PiTensorProduct.Basic

Cited by

1 results in Mathlib

Foundations

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

Assumes

CommSemiringAddCommMonoidModuleAddCommMonoidModule