Commit 2025-02-12 21:23 f78c3908

View on Github →

feat: tensor products of Hopf algebras (#12009) We define the Hopf algebra instance on a tensor product of two Hopf algebras.

Estimated changes

Modified Mathlib.lean

Modified Mathlib/Algebra/Category/HopfAlgebraCat/Basic.lean

Modified Mathlib/LinearAlgebra/TensorProduct/Basic.lean

added theorem LinearMap.lTensor_def

added theorem LinearMap.rTensor_def

added theorem TensorProduct.tensorTensorTensorComm_comp_map

Renamed Mathlib/RingTheory/HopfAlgebra.lean to Mathlib/RingTheory/HopfAlgebra/Basic.lean

Created Mathlib/RingTheory/HopfAlgebra/TensorProduct.lean

added theorem TensorProduct.antipode_def

Modified Mathlib/RingTheory/TensorProduct/Basic.lean

added theorem TensorProduct.Algebra.linearMap_comp_mul'

added theorem TensorProduct.Algebra.mul'_comp_tensorTensorTensorComm