Theorem CategoryTheory.opOp_η

Modification history

2025-06-15 16:47

Mathlib/CategoryTheory/Monoidal/Opposite.lean

chore/refactor(CategoryTheory/Monoidal/Functor): deprime LaxMonoidal and OplaxMonoidal fields (#25766) …

Deleted CategoryTheory.opOp_η View on Github →

2025-05-11 21:14

Mathlib/CategoryTheory/Monoidal/Opposite.lean

feat: `C ≌ Cᵒᵖᵒᵖ` is a monoidal equivalence (#24784) …

Added CategoryTheory.opOp_η View on Github →