Def CategoryTheory.Limits.MultispanIndex.toLinearOrderMultispanIso

Modification history

2025-04-15 16:43
Mathlib/CategoryTheory/Limits/Shapes/Multiequalizer.lean
feat(CategoryTheory/Limits): multicoequalizers attached to linear orders (#22203) …
Added CategoryTheory.Limits.MultispanIndex.toLinearOrderMultispanIsoView on Github →