Def CategoryTheory.Under.equivalenceOfIsInitial

Modification history

2025-04-09 12:22
Mathlib/CategoryTheory/Comma/Over/Basic.lean
feat: the category over a terminal object (#23702) …
Modified CategoryTheory.Under.equivalenceOfIsInitialView on Github →
2025-02-08 18:21
Mathlib/CategoryTheory/Adjunction/Over.lean
feat(Algebra/Category): adjunctions in CommRingCat (#21427)
Added CategoryTheory.Under.equivalenceOfIsInitialView on Github →