Theorem MulOpposite.counit_def

Modification history

2025-08-22 15:25

Mathlib/RingTheory/Coalgebra/MulOpposite.lean

feat(RingTheory/Coalgebra/MulOpposite): coalgebra instance for MulOpposite (#25858) …

Added MulOpposite.counit_def View on Github →