Theorem CategoryTheory.Under.mkIdInitial_to_right

Modification history

2026-02-04 20:33

Mathlib/CategoryTheory/Comma/Over/Basic.lean

feat(CategoryTheory): Being equifibered is closed under limits (#34694)

Added CategoryTheory.Under.mkIdInitial_to_right View on Github →