Commit 2025-07-11 14:29 d782e32f

View on Github →

feat: promote an AlgEquiv preserving counit and comul to a BialgEquiv (#25271) From Toric

Estimated changes

Modified Mathlib/Algebra/Algebra/Equiv.lean

modified theorem AlgEquiv.coe_ofBijective

modified theorem AlgEquiv.ofBijective_apply

added theorem AlgEquiv.toLinearMap_ofBijective

Modified Mathlib/Algebra/Algebra/Hom.lean

added theorem AlgHomClass.toLinearMap_toAlgHom

Modified Mathlib/RingTheory/Bialgebra/Equiv.lean

modified theorem BialgEquiv.coe_ofBijective

added def BialgEquiv.ofAlgEquiv

added theorem BialgEquiv.toLinearMap_ofAlgEquiv