Tensor products of Hopf algebras

We define the Hopf algebra instance on the tensor product of two Hopf algebras.

noncomputable instance TensorProduct.instHopfAlgebra {R A B : Type u} [CommRing R] [Ring A] [Ring B] [HopfAlgebra R A] [HopfAlgebra R B] : HopfAlgebra R (TensorProduct R A B)

Equations

• TensorProduct.instHopfAlgebra = HopfAlgebra.mk ⋯ ⋯

@[simp]

theorem TensorProduct.antipode_def {R A B : Type u} [CommRing R] [Ring A] [Ring B] [HopfAlgebra R A] [HopfAlgebra R B] : HopfAlgebraStruct.antipode = map HopfAlgebraStruct.antipode HopfAlgebraStruct.antipode