Commit 2024-05-16 13:54 4ee2b683

View on Github →

feat: bialgebra isomorphisms (#11971) Isomorphisms of bialgebras. Mimics Mathlib.Algebra.Module.Equiv

Estimated changes

Modified Mathlib.lean

Created Mathlib/RingTheory/Bialgebra/Equiv.lean

added def BialgEquiv.Simps.apply

added def BialgEquiv.Simps.symm_apply

added theorem BialgEquiv.coe_coe

added theorem BialgEquiv.coe_mk

added theorem BialgEquiv.coe_toAlgEquiv

added theorem BialgEquiv.coe_toBialgHom

added theorem BialgEquiv.coe_toCoalgEquiv

added theorem BialgEquiv.coe_toEquiv_symm

added theorem BialgEquiv.coe_toEquiv_trans

added theorem BialgEquiv.ext

added theorem BialgEquiv.ext_iff

added theorem BialgEquiv.invFun_eq_symm

added def BialgEquiv.refl

added theorem BialgEquiv.refl_toBialgHom

added theorem BialgEquiv.refl_toCoalgEquiv

added def BialgEquiv.symm

added theorem BialgEquiv.symm_toCoalgEquiv

added def BialgEquiv.toAlgEquiv

added theorem BialgEquiv.toAlgEquiv_eq_coe

added def BialgEquiv.toBialgHom

added theorem BialgEquiv.toBialgHom_eq_coe

added theorem BialgEquiv.toBialgHom_inj

added theorem BialgEquiv.toBialgHom_injective

added theorem BialgEquiv.toBialgHom_toAlgHom

added theorem BialgEquiv.toCoalgEquiv_eq_coe

added theorem BialgEquiv.toCoalgEquiv_toCoalgHom

added def BialgEquiv.toEquiv

added theorem BialgEquiv.toEquiv_inj

added theorem BialgEquiv.toEquiv_injective

added def BialgEquiv.trans

added theorem BialgEquiv.trans_toBialgHom

added theorem BialgEquiv.trans_toCoalgEquiv

added structure BialgEquiv

added def BialgEquivClass.toBialgEquiv

Modified Mathlib/RingTheory/Coalgebra/Equiv.lean