Theorems · Theorem · ring theory

Bialgebra.TensorProduct.assoc_tmul

∀ {R : Type u_1} {S : Type u_2} {A : Type u_3} {C : Type u_5} {D : Type u_6} [inst : CommSemiring R]
  [inst_1 : CommSemiring S] [inst_2 : Semiring A] [inst_3 : Bialgebra S A] [inst_4 : Algebra R A] [inst_5 : Algebra R S]
  [inst_6 : IsScalarTower R S A] [inst_7 : Semiring C] [inst_8 : Semiring D] [inst_9 : Bialgebra S C]
  [inst_10 : Bialgebra R D] [inst_11 : Algebra R C] [inst_12 : IsScalarTower R S C] (x : A) (y : C) (z : D),
  (Bialgebra.TensorProduct.assoc R S A C D) (x ⊗ₜ[S] y ⊗ₜ[R] z) = x ⊗ₜ[S] (y ⊗ₜ[R] z)

Defined in

Mathlib.RingTheory.Bialgebra.TensorProduct

Cited by

0 results in Mathlib

Foundations

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

Assumes

CommSemiringCommSemiringSemiringBialgebraAlgebraAlgebraIsScalarTowerSemiringSemiringBialgebraBialgebraAlgebraIsScalarTower