Theorems · Definition · ring theory

Bialgebra.TensorProduct.comm

(R : Type u_1) →
  (A : Type u_3) →
    (B : Type u_4) →
      [inst : CommSemiring R] →
        [inst_1 : Semiring A] →
          [inst_2 : Semiring B] →
            [inst_3 : Bialgebra R A] → [inst_4 : Bialgebra R B] → TensorProduct R A B ≃ₐc[R] TensorProduct R B A

The tensor product of R-bialgebras is commutative, up to bialgebra isomorphism.

Defined in

Mathlib.RingTheory.Bialgebra.TensorProduct

Cited by

1 results in Mathlib

Foundations

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

Assumes

CommSemiringSemiringSemiringBialgebraBialgebra