Theorem CategoryTheory.IsPushout.of_iso'

Modification history

2026-01-15 20:10

Mathlib/CategoryTheory/Limits/Shapes/Pullback/CommSq.lean

chore(CategoryTheory/Limits/Shapes/Pullback): Split `CommSq` (#33968) …

Modified CategoryTheory.IsPushout.of_iso'View on Github →

2025-12-05 16:31

Mathlib/CategoryTheory/Limits/Shapes/Pullback/CommSq.lean

feat(AlgebraicTopology): horns in `Δ[2]` as pushouts (#31802) …

Added CategoryTheory.IsPushout.of_iso'View on Github →