Commit 2023-06-14 07:51 d8c9d310

View on Github →

feat: port Algebra.Homology.Module (#5000)

Estimated changes

Modified Mathlib.lean

Modified Mathlib/Algebra/Category/ModuleCat/Subobject.lean

Modified Mathlib/Algebra/Homology/ImageToKernel.lean

added theorem homology.π_map_apply

added theorem imageToKernel_arrow_apply

Created Mathlib/Algebra/Homology/ModuleCat.lean

added theorem ModuleCat.cyclesMap_toCycles

added theorem ModuleCat.cycles_ext

added theorem ModuleCat.homology_ext'

added theorem ModuleCat.homology_ext