Def CategoryTheory.Limits.pasteHorizIsPushout

Modification history

2024-08-04 10:58

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

feat(Limits/Shapes/Pullback): add more pasting lemmas (#14414) …

Added CategoryTheory.Limits.pasteHorizIsPushout View on Github →