Commit 2025-05-11 21:14 41c20816

View on Github →

feat: C ≌ Cᵒᵖᵒᵖ is a monoidal equivalence (#24784) From Toric

Estimated changes

Modified Mathlib/CategoryTheory/Monoidal/Opposite.lean

added theorem CategoryTheory.opOp_δ

added theorem CategoryTheory.opOp_ε

added theorem CategoryTheory.opOp_η

added theorem CategoryTheory.opOp_μ

added theorem CategoryTheory.unopUnop_δ

added theorem CategoryTheory.unopUnop_ε

added theorem CategoryTheory.unopUnop_η

added theorem CategoryTheory.unopUnop_μ