Commit 2025-07-14 05:34 8e7f51e0

View on Github →

feat(Bialgebra/Equiv): basic lemmas (#27041) From Toric

Estimated changes

Modified Mathlib/RingTheory/Bialgebra/Equiv.lean

added theorem BialgEquiv.apply_symm_apply

modified theorem BialgEquiv.coe_mk

added theorem BialgEquiv.comp_symm

added theorem BialgEquiv.symm_apply_apply

added theorem BialgEquiv.symm_comp

added theorem BialgEquiv.toAlgEquiv_toRingHom

added theorem BialgEquiv.toRingEquiv_toRingHom

Modified Mathlib/RingTheory/Bialgebra/Hom.lean