Commit 2025-11-21 11:20 d249a60b

View on Github →

feat(CategoryTheory/ComposableArrows): compositions of 1 or 2 morphisms (#31588)

Estimated changes

Modified Mathlib.lean

Created Mathlib/CategoryTheory/ComposableArrows/One.lean

Created Mathlib/CategoryTheory/ComposableArrows/Two.lean

added def CategoryTheory.ComposableArrows.twoδ₁Toδ₀

added theorem CategoryTheory.ComposableArrows.twoδ₁Toδ₀_app_one

added theorem CategoryTheory.ComposableArrows.twoδ₁Toδ₀_app_zero

added def CategoryTheory.ComposableArrows.twoδ₂Toδ₁

added theorem CategoryTheory.ComposableArrows.twoδ₂Toδ₁_app_one

added theorem CategoryTheory.ComposableArrows.twoδ₂Toδ₁_app_zero