Def CategoryTheory.LiftRightAdjoint.unitEqualises

Modification history

2024-09-03 09:13

Mathlib/CategoryTheory/Adjunction/Lifting/Right.lean

feat(CategoryTheory/Adjunction): dualize adjoint lifting theorem (#16066) …

Added CategoryTheory.LiftRightAdjoint.unitEqualises View on Github →