Theorems · Definition · linear algebra

TensorProduct.directSumRight

(R : Type u) →
  [inst : CommSemiring R] →
    (S : Type u_1) →
      [inst_1 : Semiring S] →
        [inst_2 : Algebra R S] →
          {ι₂ : Type v₂} →
            [DecidableEq ι₂] →
              (M₁' : Type w₁') →
                (M₂ : ι₂ → Type w₂) →
                  [inst_4 : AddCommMonoid M₁'] →
                    [inst_5 : (i₂ : ι₂) → AddCommMonoid (M₂ i₂)] →
                      [inst_6 : Module R M₁'] →
                        [inst_7 : (i₂ : ι₂) → Module R (M₂ i₂)] →
                          [inst_8 : Module S M₁'] →
                            [inst_9 : IsScalarTower R S M₁'] →
                              TensorProduct R M₁' (DirectSum ι₂ fun i => M₂ i) ≃ₗ[S]
                                DirectSum ι₂ fun i => TensorProduct R M₁' (M₂ i)

Tensor products distribute over a direct sum on the right.

Defined in

Mathlib.LinearAlgebra.DirectSum.TensorProduct

Cited by

12 results in Mathlib

Foundations

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

Assumes

CommSemiringSemiringAlgebraDecidableEqAddCommMonoidAddCommMonoidModuleModuleModuleIsScalarTower