Commit 2026-03-09 18:53 c7113cf4

View on Github →

refactor(CategoryTheory/Limits/Shapes/Kernels): define zeroKernelFork using KernelFork.ofι (#36409) I think this is a more natural definition with better defeqs.

Estimated changes

Modified Mathlib/CategoryTheory/Limits/Shapes/Kernels.lean

modified def CategoryTheory.Limits.cokernel.zeroCokernelCofork

added theorem CategoryTheory.Limits.cokernel.zeroCokernelCofork_π

modified def CategoryTheory.Limits.kernel.zeroKernelFork

added theorem CategoryTheory.Limits.kernel.zeroKernelFork_ι