Theorem CategoryTheory.ShortComplex.π₁Toπ₂_comp_π₂Toπ₃

Modification history

2025-08-05 23:45
Mathlib/Algebra/Homology/ShortComplex/Basic.lean
feat: replace aesop_cat with a configurable discharger (#27938) …
Modified CategoryTheory.ShortComplex.π₁Toπ₂_comp_π₂Toπ₃View on Github →
2023-05-24 10:36
Mathlib/Algebra/Homology/ShortComplex/Basic.lean
feat: Algebra.Homology.ShortComplex.Basic (#4203) …
Added CategoryTheory.ShortComplex.π₁Toπ₂_comp_π₂Toπ₃View on Github →