Commit 2022-02-24 03:44 f3ee4628

View on Github →

chore(category_theory/adjunction/opposites): Forgotten category_theory namespace (#12256) The forgotten category_theory namespace means that dot notation doesn't work on category_theory.adjunction.

Estimated changes