Commit 2023-12-05 00:40 befd8b23

View on Github →

feat(RingTheory): coalgebra definition (#8621) Add definition and example of a coalgebra.

Estimated changes

Modified Mathlib.lean

Created Mathlib/RingTheory/Coalgebra.lean

added theorem Coalgebra.coassoc_apply

added theorem Coalgebra.coassoc_symm

added theorem Coalgebra.coassoc_symm_apply

added theorem Coalgebra.lTensor_counit_comul

added theorem Coalgebra.rTensor_counit_comul

added theorem CommSemiring.comul_apply

added theorem CommSemiring.counit_apply

added theorem Finsupp.comul_single

added theorem Finsupp.counit_single