Commit 2026-01-30 15:11 dd5024f3

View on Github →

chore(CategoryTheory/Adjunction): slightly generalize universes in adjoint functor theorem (#34541) Also updates a name in the module docstring

Estimated changes

Modified Mathlib/CategoryTheory/Adjunction/AdjointFunctorTheorems.lean

modified def CategoryTheory.SolutionSetCondition

modified theorem CategoryTheory.solutionSetCondition_of_isRightAdjoint