mathlib
f3ee4628 - chore(category_theory/adjunction/opposites): Forgotten `category_theory` namespace (#12256)

Commit
3 years ago
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`.
Author
Parents
Loading