Theorems · Theorem · linear algebra

TensorProduct.directSumRight_tmul_lof

∀ (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 : 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₁'] (x : M₁') (i : ι₂) (y : M₂ i),
  (TensorProduct.directSumRight R S M₁' M₂) (x ⊗ₜ[R] (DirectSum.lof R ι₂ M₂ i) y) =
    (DirectSum.lof S ι₂ (fun i => TensorProduct R M₁' (M₂ i)) i) (x ⊗ₜ[R] y)

Defined in

Mathlib.LinearAlgebra.DirectSum.TensorProduct

Cited by

4 results in Mathlib

Foundations

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

Assumes

CommSemiringSemiringAlgebraDecidableEqAddCommMonoidAddCommMonoidModuleModuleModuleIsScalarTower