Commit 2023-05-25 08:46 e9d2bc8d

View on Github →

feat: port Algebra.Category.Module.Abelian (#4299)

Estimated changes

Modified Mathlib.lean

Created Mathlib/Algebra/Category/ModuleCat/Abelian.lean

added theorem ModuleCat.exact_iff

added def ModuleCat.normalEpi

added def ModuleCat.normalMono