Theorem CategoryTheory.obj_ext_of_isDiscrete

Modification history

2025-05-24 09:54
Mathlib/CategoryTheory/Discrete/Basic.lean
feat(CategoryTheory): `IsDiscrete` implies `IsGroupoid` (#25136) …
Modified CategoryTheory.obj_ext_of_isDiscreteView on Github →
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 →