Def CategoryTheory.StructuredArrow.ofStructuredArrowProjEquivalence.functor

Modification history

2024-09-03 13:17

Mathlib/CategoryTheory/Comma/Over.lean

feat(CategoryTheory): Characterization of Structured Arrows of Diagonal and Projections (#15838)

Added CategoryTheory.StructuredArrow.ofStructuredArrowProjEquivalence.functor View on Github →