Commit 2026-03-22 21:26 7d7b49d3

View on Github →

chore(CategoryTheory/Opposites): use to_dual self (#36809) This PR tags various declarations in about ᵒᵖ in category theory with to_dual self, so that these can be translated with to_dual.

Estimated changes

modified theorem Quiver.Hom.unop_mk