Commit 2025-09-01 07:31 23ec09de

View on Github →

feat: upgrade a bialgebra to a Hopf algebra by giving the antipode as an AlgHom (#29155) From Toric

Estimated changes

Modified Mathlib/RingTheory/HopfAlgebra/TensorProduct.lean

Modified Mathlib/RingTheory/TensorProduct/Basic.lean

added theorem Algebra.TensorProduct.lmul'_comp_map