mathlib

4dabfb92 - chore(category_theory): better definitional properties for kernel_lift (#17328)

chore(category_theory): better definitional properties for kernel_lift (#17328) This PR makes `kernel.lift` definitionally equal to the application of `(kernel_is_kernel f).lift`, and similarly for `cokernel.desc`.