Theorem CategoryTheory.Limits.pullbackIsoUnopPushout_inv_snd

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.pullbackIsoUnopPushout_inv_sndView on Github →
2025-10-15 10:06
Mathlib/CategoryTheory/Limits/Opposites.lean
chore(CategoryTheory/Limits/Opposites): split the file Limits.Opposites (#30517) …
Modified CategoryTheory.Limits.pullbackIsoUnopPushout_inv_sndView on Github →
2023-03-11 16:29
Mathlib/CategoryTheory/Limits/Opposites.lean
feat: port CategoryTheory.Limits.Opposites (#2805)
Added CategoryTheory.Limits.pullbackIsoUnopPushout_inv_sndView on Github →