Def CategoryTheory.LiftRightAdjoint.unitEqualises

Modification history

2026-10-07 01:57
Mathlib/CategoryTheory/Adjunction/Lifting/Right.lean
chore: rename `unitEqualises` and `counitCoequalises` to American spelling (#44520) …
Deleted CategoryTheory.LiftRightAdjoint.unitEqualisesView on Github →
2025-12-01 06:24
Mathlib/CategoryTheory/Adjunction/Lifting/Right.lean
refactor(Category Theory): change `RegularMono`/`Epi` from class to structure (#32154) …
Modified CategoryTheory.LiftRightAdjoint.unitEqualisesView on Github →
2024-09-03 09:13
Mathlib/CategoryTheory/Adjunction/Lifting/Right.lean
feat(CategoryTheory/Adjunction): dualize adjoint lifting theorem (#16066) …
Added CategoryTheory.LiftRightAdjoint.unitEqualisesView on Github →