Theorem CategoryTheory.Limits.isIndObject_iff_preservesFiniteLimits

Modification history

2025-02-06 15:22
Mathlib/CategoryTheory/Limits/Indization/IndObject.lean
feat(CategoryTheory): equivalence between `Ind C` and left exact functors from `C` to `Type` (#21430)
Added CategoryTheory.Limits.isIndObject_iff_preservesFiniteLimitsView on Github →