Theorems · Theorem · linear algebra

TensorProduct.restrictScalar_directSumRight

∀ (R : Type u) [inst : CommSemiring R] (S : Type u_2) [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₁'] (S₀ : Type u_1) [inst_10 : CommSemiring S₀]
  [inst_11 : Algebra R S₀] [inst_12 : Algebra S₀ S] [inst_13 : Module S₀ M₁'] [inst_14 : IsScalarTower R S₀ M₁']
  [inst_15 : IsScalarTower S₀ S M₁'],
  LinearEquiv.restrictScalars S₀ (TensorProduct.directSumRight R S M₁' M₂) = TensorProduct.directSumRight R S₀ M₁' M₂

Defined in

Mathlib.LinearAlgebra.DirectSum.TensorProduct

Cited by

2 results in Mathlib

Foundations

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

Assumes

CommSemiringSemiringAlgebraDecidableEqAddCommMonoidAddCommMonoidModuleModuleModuleIsScalarTowerCommSemiringAlgebraAlgebraModuleIsScalarTowerIsScalarTower