Def CategoryTheory.LiftLeftAdjoint.counitCoequalises

Modification history

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