Commit 2023-06-12 08:12 889ec590

View on Github →

feat: port Algebra.Category.Module.Subobject (#4224)

Estimated changes

Modified Mathlib.lean

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

added theorem ModuleCat.cokernel_π_imageSubobject_ext

added theorem ModuleCat.toKernelSubobject_arrow