Theorems · Definition · linear algebra

TensorProduct.piLeft

(R : Type u_1) →
  [inst : CommSemiring R] →
    (N : Type u_3) →
      [inst_1 : AddCommMonoid N] →
        [inst_2 : Module R N] →
          {ι : Type u_4} →
            (M : ι → Type u_5) →
              [inst_3 : (i : ι) → AddCommMonoid (M i)] →
                [inst_4 : (i : ι) → Module R (M i)] →
                  [Fintype ι] →
                    [DecidableEq ι] → TensorProduct R ((i : ι) → M i) N ≃ₗ[R] (i : ι) → TensorProduct R (M i) N

Tensor product commutes with finite products on the left. TODO: generalize to S-linear.

Defined in

Mathlib.LinearAlgebra.TensorProduct.Pi

Cited by

1 results in Mathlib

Foundations

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

Assumes

CommSemiringAddCommMonoidModuleAddCommMonoidModuleFintypeDecidableEq