Commit 2025-04-09 15:25 e3c93add

View on Github →

refactor: don't expose the functor (Over X)ᵒᵖ ⥤ Under (op X) (#23839) Instead only expose the equivalence. From Toric

Estimated changes

Modified Mathlib/CategoryTheory/Comma/Over/Basic.lean

modified def CategoryTheory.Over.opToOpUnder

modified def CategoryTheory.Over.opToUnderOp

modified def CategoryTheory.Under.opToOpOver

modified def CategoryTheory.Under.opToOverOp