Commit 2024-05-02 14:08 22b9916c

View on Github →

feat: coalgebra isomorphisms (#11970) Isomorphisms of coalgebras. Mimics Mathlib.Algebra.Module.Equiv.

Estimated changes

Modified Mathlib.lean

Modified Mathlib/LinearAlgebra/Basic.lean

added theorem LinearEquiv.ofLinear_symm_toLinearMap

added theorem LinearEquiv.ofLinear_toLinearMap

Created Mathlib/RingTheory/Coalgebra/Equiv.lean

added def CoalgEquiv.Simps.apply

added def CoalgEquiv.Simps.symm_apply

added theorem CoalgEquiv.coe_coe

added theorem CoalgEquiv.coe_mk

added theorem CoalgEquiv.coe_toCoalgHom

added theorem CoalgEquiv.coe_toEquiv_symm

added theorem CoalgEquiv.coe_toEquiv_trans

added theorem CoalgEquiv.coe_toLinearEquiv

added theorem CoalgEquiv.ext

added theorem CoalgEquiv.ext_iff

added theorem CoalgEquiv.invFun_eq_symm

added def CoalgEquiv.refl

added theorem CoalgEquiv.refl_toCoalgHom

added theorem CoalgEquiv.refl_toLinearEquiv

added def CoalgEquiv.symm

added theorem CoalgEquiv.symm_toCoalgHom

added theorem CoalgEquiv.symm_toLinearEquiv

added theorem CoalgEquiv.toCoalgHom_eq_coe

added theorem CoalgEquiv.toCoalgHom_inj

added theorem CoalgEquiv.toCoalgHom_injective

added def CoalgEquiv.toEquiv

added theorem CoalgEquiv.toEquiv_inj

added theorem CoalgEquiv.toEquiv_injective

added theorem CoalgEquiv.toLinearEquiv_eq_coe

added theorem CoalgEquiv.toLinearEquiv_toLinearMap

added def CoalgEquiv.trans

added theorem CoalgEquiv.trans_toCoalgHom

added theorem CoalgEquiv.trans_toLinearEquiv

added structure CoalgEquiv

added def CoalgEquivClass.toCoalgEquiv