Def CategoryTheory.StructuredArrow.ofDiagEquivalence'

Modification history

2026-04-13 19:44

Mathlib/CategoryTheory/Comma/Over/Basic.lean

chore(CategoryTheory/Comma): API separation for StructuredArrow (#37809) …

Added CategoryTheory.StructuredArrow.ofDiagEquivalence'View on Github →

2024-12-09 19:23

Mathlib/CategoryTheory/Comma/Over.lean

perf: mark some definitions as non-computable (#19740) …

Deleted CategoryTheory.StructuredArrow.ofDiagEquivalence'View on Github →

2024-09-03 13:17

Mathlib/CategoryTheory/Comma/Over.lean

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

Added CategoryTheory.StructuredArrow.ofDiagEquivalence'View on Github →