Commit 2025-11-05 13:09 26d3788a

View on Github →

feat(Algebra/Homology/ShortComplex): functoriality of first/second map (#31249) From ClassFieldTheory

Estimated changes

Modified Mathlib/Algebra/Homology/ShortComplex/Basic.lean

added def CategoryTheory.ShortComplex.fFunctor

added def CategoryTheory.ShortComplex.gFunctor

added theorem CategoryTheory.ShortComplex.map_comp

added theorem CategoryTheory.ShortComplex.map_id

modified structure CategoryTheory.ShortComplex