Commit 2023-11-01 06:34 350a3748

View on Github →

feat(CategoryTheory): the category of composable arrows (#7999)

Estimated changes

Modified Mathlib.lean

Created Mathlib/CategoryTheory/ComposableArrows.lean

added def CategoryTheory.ComposableArrows.Mk₁.map

added theorem CategoryTheory.ComposableArrows.Mk₁.map_comp

added theorem CategoryTheory.ComposableArrows.Mk₁.map_id

added def CategoryTheory.ComposableArrows.Mk₁.obj

added theorem CategoryTheory.ComposableArrows.map'_comp

added theorem CategoryTheory.ComposableArrows.map'_self

added def CategoryTheory.ComposableArrows.mk₀

added def CategoryTheory.ComposableArrows.mk₁

added theorem CategoryTheory.nerve_obj_eq_composableArrows

Modified Mathlib/Data/Fin/Basic.lean

added theorem Fin.eq_one_of_neq_zero