Theorems · Theorem · ring theory

TensorProduct.AlgebraTensorModule.tensorTensorTensorComm.congr_simp

∀ (R : Type uR) (S : Type uS) (A : Type uA) (B : Type uB) (M : Type uM) (N : Type uN) (P : Type uP) (Q : Type uQ)
  [inst : CommSemiring R] [inst_1 : CommSemiring A] [inst_2 : Semiring B] [inst_3 : Algebra R A] [inst_4 : Algebra R B]
  [inst_5 : AddCommMonoid M] [inst_6 : Module R M] [inst_7 : Module A M] [inst_8 : Module B M]
  [inst_9 : IsScalarTower R A M] [inst_10 : IsScalarTower R B M] [inst_11 : SMulCommClass A B M]
  [inst_12 : AddCommMonoid N] [inst_13 : Module R N] [inst_14 : AddCommMonoid P] [inst_15 : Module A P]
  [inst_16 : AddCommMonoid Q] [inst_17 : Module R Q] [inst_18 : Module R P] [inst_19 : IsScalarTower R A P]
  [inst_20 : Algebra A B] [inst_21 : IsScalarTower A B M] [inst_22 : CommSemiring S] [inst_23 : Algebra R S]
  [inst_24 : Algebra S B] [inst_25 : Module S M] [inst_26 : Module S N] [inst_27 : IsScalarTower R S M]
  [inst_28 : SMulCommClass A S M] [inst_29 : SMulCommClass S A M] [inst_30 : IsScalarTower S B M]
  [inst_31 : IsScalarTower R S N],
  TensorProduct.AlgebraTensorModule.tensorTensorTensorComm R S A B M N P Q =
    TensorProduct.AlgebraTensorModule.tensorTensorTensorComm R S A B M N P Q

Defined in

Mathlib.RingTheory.TensorProduct.Maps

Cited by

0 results in Mathlib

Foundations

Depth 77 from the axioms · uses propext, Quot.sound

Assumes

CommSemiringCommSemiringSemiringAlgebraAlgebraAddCommMonoidModuleModuleModuleIsScalarTowerIsScalarTowerSMulCommClassAddCommMonoidModuleAddCommMonoidModuleAddCommMonoidModuleModuleIsScalarTowerAlgebraIsScalarTowerCommSemiringAlgebraAlgebraModuleModuleIsScalarTowerSMulCommClassSMulCommClassIsScalarTowerIsScalarTower