Commit 2023-04-18 11:25 f0717727

View on Github →

feat: port Algebra.Homology.Functor (#3493)

Estimated changes

Modified Mathlib.lean

Created Mathlib/Algebra/Homology/Functor.lean

added def HomologicalComplex.asFunctor

added def HomologicalComplex.complexOfFunctorsToFunctorToComplex