Theorems · Theorem · ring theory

Algebra.TensorProduct.assoc_tmul

∀ (R : Type uR) (S : Type uS) {T : Type u_2} (A : Type uA) {C : Type uC} {D : Type uD} [inst : CommSemiring R]
  [inst_1 : CommSemiring S] [inst_2 : Algebra R S] [inst_3 : Semiring A] [inst_4 : Algebra R A] [inst_5 : Algebra S A]
  [inst_6 : IsScalarTower R S A] [inst_7 : Semiring C] [inst_8 : Algebra R C] [inst_9 : Algebra S C]
  [inst_10 : IsScalarTower R S C] [inst_11 : Semiring D] [inst_12 : Algebra R D] [inst_13 : CommSemiring T]
  [inst_14 : Algebra R T] [inst_15 : Algebra S T] [inst_16 : Algebra T A] [inst_17 : IsScalarTower R T A]
  [inst_18 : IsScalarTower S T A] (a : A) (b : C) (c : D),
  (Algebra.TensorProduct.assoc R S T A C D) (a ⊗ₜ[S] b ⊗ₜ[R] c) = a ⊗ₜ[S] (b ⊗ₜ[R] c)

Defined in

Mathlib.RingTheory.TensorProduct.Maps

Cited by

0 results in Mathlib

Foundations

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

Assumes

CommSemiringCommSemiringAlgebraSemiringAlgebraAlgebraIsScalarTowerSemiringAlgebraAlgebraIsScalarTowerSemiringAlgebraCommSemiringAlgebraAlgebraAlgebraIsScalarTowerIsScalarTower