Theorem CategoryTheory.Limits.coend.map_id

Modification history

2025-08-05 23:45
Mathlib/CategoryTheory/Limits/Shapes/End.lean
feat: replace aesop_cat with a configurable discharger (#27938) …
Modified CategoryTheory.Limits.coend.map_idView on Github →
2025-07-14 10:55
Mathlib/CategoryTheory/Limits/Shapes/End.lean
feat(CategoryTheory/Limits/Shapes/End): functoriality of (co)ends (#27079) …
Added CategoryTheory.Limits.coend.map_idView on Github →