mathlib3

f33418a9 - feat(algebra/homology/chain_complex): pushforward of complex w.r.t. additive functor (#6403)

feat(algebra/homology/chain_complex): pushforward of complex w.r.t. additive functor (#6403) This PR adds a definition for the pushforward of a homological complex with respect to an additive functor.