Theorem CategoryTheory.Limits.IsIndObject.iff_of_iso

Modification history

2026-04-14 15:27
Mathlib/CategoryTheory/Limits/Indization/IndObject.lean
refactor(CategoryTheory): one-field structure morphisms in the category of types (#36613) …
Modified CategoryTheory.Limits.IsIndObject.iff_of_isoView on Github →
2024-03-24 20:38
Mathlib/CategoryTheory/Limits/Indization/IndObject.lean
feat: ind-objects are closed under isomorphism (#11623)
Added CategoryTheory.Limits.IsIndObject.iff_of_isoView on Github →