Theorems · Theorem · linear algebra

TensorProduct.directSum_lof_tmul_lof

∀ (R : Type u) [inst : CommSemiring R] (S : Type u_1) [inst_1 : Semiring S] [inst_2 : Algebra R S] {ι₁ : Type v₁}
  {ι₂ : Type v₂} [inst_3 : DecidableEq ι₁] [inst_4 : DecidableEq ι₂] {M₁ : ι₁ → Type w₁} {M₂ : ι₂ → Type w₂}
  [inst_5 : (i₁ : ι₁) → AddCommMonoid (M₁ i₁)] [inst_6 : (i₂ : ι₂) → AddCommMonoid (M₂ i₂)]
  [inst_7 : (i₁ : ι₁) → Module R (M₁ i₁)] [inst_8 : (i₂ : ι₂) → Module R (M₂ i₂)]
  [inst_9 : (i₁ : ι₁) → Module S (M₁ i₁)] [inst_10 : ∀ (i₁ : ι₁), IsScalarTower R S (M₁ i₁)] (i₁ : ι₁) (m₁ : M₁ i₁)
  (i₂ : ι₂) (m₂ : M₂ i₂),
  (TensorProduct.directSum R S M₁ M₂) ((DirectSum.lof S ι₁ M₁ i₁) m₁ ⊗ₜ[R] (DirectSum.lof R ι₂ M₂ i₂) m₂) =
    (DirectSum.lof S (ι₁ × ι₂) (fun i => TensorProduct R (M₁ i.1) (M₂ i.2)) (i₁, i₂)) (m₁ ⊗ₜ[R] m₂)

Defined in

Mathlib.LinearAlgebra.DirectSum.TensorProduct

Cited by

5 results in Mathlib

Foundations

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

Assumes

CommSemiringSemiringAlgebraDecidableEqDecidableEqAddCommMonoidAddCommMonoidModuleModuleModuleIsScalarTower