Theorem CategoryTheory.Limits.pullbackIsoOpPushout_inv_fst

Modification history

2026-02-17 21:47

Mathlib/CategoryTheory/Limits/Shapes/Opposites/Pullbacks.lean

chore(CategoryTheory/Limits): add instances for `HasPullback f.op g.op` and `HasPushout f.op g.op` (#35453) …

Modified CategoryTheory.Limits.pullbackIsoOpPushout_inv_fst View on Github →

2025-10-21 12:12

Mathlib/CategoryTheory/Limits/Shapes/Opposites/Pullbacks.lean

feat(CategoryTheory/Limits/Opposites) : add opposites of coforks and forks (#30200) …

Added CategoryTheory.Limits.pullbackIsoOpPushout_inv_fst View on Github →