Theorem CategoryTheory.Limits.IsIPCOfShape.of_isIso

Modification history

2026-05-06 00:44

Mathlib/CategoryTheory/Limits/FilteredColimitCommutesProduct.lean

refactor(CategoryTheory/Limits): redefine `IsIPC` in terms of `IsIPCOfShape` (#38378) …

Added CategoryTheory.Limits.IsIPCOfShape.of_isIso View on Github →