mathlib

2dcc307e - feat(category_theory/limits): morphism to terminal is split mono (#8084)

feat(category_theory/limits): morphism to terminal is split mono (#8084) A generalisation of existing results: we already have an instance `split_mono` to `mono` so this is strictly more general.