Def CategoryTheory.Limits.Pi.functorπ

Modification history

2026-05-06 00:44

Mathlib/CategoryTheory/Limits/Shapes/Products.lean

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

Added CategoryTheory.Limits.Pi.functorπ View on Github →