Theorems · Theorem · linear algebra

TensorProduct.directSumLeft_tmul

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

Defined in

Mathlib.LinearAlgebra.DirectSum.TensorProduct

Cited by

0 results in Mathlib

Foundations

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

Assumes

CommSemiringSemiringAlgebraDecidableEqAddCommMonoidAddCommMonoidModuleModuleModuleIsScalarTower