Theorem CategoryTheory.Abelian.SpectralObject.mapFourδ₁Toδ₀'_mapFourδ₃Toδ₃'

Modification history

2026-03-12 17:39
Mathlib/Algebra/Homology/SpectralObject/EpiMono.lean
feat(Algebra/Homology/SpectralObject): induced morphisms that are epi/mono (#36153)
Added CategoryTheory.Abelian.SpectralObject.mapFourδ₁Toδ₀'_mapFourδ₃Toδ₃'View on Github →