Commit 2023-03-09 06:58 2402232c

View on Github →

feat: port CategoryTheory.Preadditive.Basic (#2735)

Estimated changes

Modified Mathlib.lean

Created Mathlib/CategoryTheory/Preadditive/Basic.lean

added theorem CategoryTheory.Preadditive.IsIso.comp_left_eq_zero

added theorem CategoryTheory.Preadditive.IsIso.comp_right_eq_zero

added def CategoryTheory.Preadditive.coforkOfCokernelCofork

added theorem CategoryTheory.Preadditive.coforkOfCokernelCofork_π

added def CategoryTheory.Preadditive.cokernelCoforkOfCofork

added theorem CategoryTheory.Preadditive.cokernelCoforkOfCofork_ofπ

added theorem CategoryTheory.Preadditive.cokernelCoforkOfCofork_π

added def CategoryTheory.Preadditive.compHom

added theorem CategoryTheory.Preadditive.comp_neg

added theorem CategoryTheory.Preadditive.comp_nsmul

added theorem CategoryTheory.Preadditive.comp_sub

added theorem CategoryTheory.Preadditive.comp_sum

added theorem CategoryTheory.Preadditive.comp_zsmul

added theorem CategoryTheory.Preadditive.epi_iff_cancel_zero

added theorem CategoryTheory.Preadditive.epi_of_cancel_zero

added theorem CategoryTheory.Preadditive.epi_of_cokernel_iso_zero

added theorem CategoryTheory.Preadditive.epi_of_cokernel_zero

added def CategoryTheory.Preadditive.forkOfKernelFork

added theorem CategoryTheory.Preadditive.forkOfKernelFork_ι

added theorem CategoryTheory.Preadditive.hasCoequalizer_of_hasCokernel

added theorem CategoryTheory.Preadditive.hasCoequalizers_of_hasCokernels

added theorem CategoryTheory.Preadditive.hasCokernel_of_hasCoequalizer

added theorem CategoryTheory.Preadditive.hasEqualizer_of_hasKernel

added theorem CategoryTheory.Preadditive.hasEqualizers_of_hasKernels

added theorem CategoryTheory.Preadditive.hasKernel_of_hasEqualizer

added def CategoryTheory.Preadditive.isColimitCoforkOfCokernelCofork

added theorem CategoryTheory.Preadditive.isColimitCoforkOfCokernelCofork_desc

added def CategoryTheory.Preadditive.isColimitCokernelCoforkOfCofork

added def CategoryTheory.Preadditive.isLimitForkOfKernelFork

added theorem CategoryTheory.Preadditive.isLimitForkOfKernelFork_lift

added def CategoryTheory.Preadditive.isLimitKernelForkOfFork

added def CategoryTheory.Preadditive.kernelForkOfFork

added theorem CategoryTheory.Preadditive.kernelForkOfFork_ofι

added theorem CategoryTheory.Preadditive.kernelForkOfFork_ι

added def CategoryTheory.Preadditive.leftComp

added theorem CategoryTheory.Preadditive.mono_iff_cancel_zero

added theorem CategoryTheory.Preadditive.mono_of_cancel_zero

added theorem CategoryTheory.Preadditive.mono_of_kernel_iso_zero

added theorem CategoryTheory.Preadditive.mono_of_kernel_zero

added theorem CategoryTheory.Preadditive.neg_comp

added theorem CategoryTheory.Preadditive.neg_comp_neg

added theorem CategoryTheory.Preadditive.nsmul_comp

added def CategoryTheory.Preadditive.rightComp

added theorem CategoryTheory.Preadditive.sub_comp

added theorem CategoryTheory.Preadditive.sum_comp

added theorem CategoryTheory.Preadditive.zsmul_comp