Mathlib Changelog
v4
Changelog
About
Github
Commit
2025-12-24 14:13
3137715b
View on Github →
chore(RingTheory/Coalgebra/MonoidAlgebra): use
to_additive
(
#33141
)
Estimated changes
Modified
Mathlib/RingTheory/Coalgebra/MonoidAlgebra.lean
deleted
theorem
AddMonoidAlgebra.comul_single
deleted
theorem
AddMonoidAlgebra.counit_single