Theorem CategoryTheory.Arrow.ext

Modification history

2025-02-03 05:29
Mathlib/CategoryTheory/Comma/Arrow.lean
feat(CategoryTheory): the class of morphisms given by a family of maps (#21354) …
Modified CategoryTheory.Arrow.extView on Github →
2025-01-21 18:15
Mathlib/CategoryTheory/Comma/Arrow.lean
feat(CategoryTheory): `Arrow A` is finite iff `A` is a finite category (#19945) …
Added CategoryTheory.Arrow.extView on Github →