Theorem CategoryTheory.obj_ext_of_isDiscrete

Modification history

2024-10-25 15:10
Mathlib/CategoryTheory/DiscreteCategory.lean
feat(CategoryTheory): constructor for pseudofunctors from a strict locally discrete category (#18201) …
Added CategoryTheory.obj_ext_of_isDiscreteView on Github →