Def CategoryTheory.Arrow.equivSigma

Modification history

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.equivSigma View on Github →