Commit 2026-07-01 07:16 a05b35ba

refactor(CategoryTheory/Limits/Shape/Kernels): remove duplicate lemma (#41207) Lemma Limits.kernel.ι_of_zero was saying the same thing as instance Limits.kernel.ι_zero_isIso, that is, that kernel.ι 0 is an isomorphism; the proofs were also identical. Rewrite the lemma to make it say that kernel.ι f is an isomorphism provided that f = 0; this follows immediately from equalizer.ι_of_eq but might still be useful. Same with Limits.cokernel.π_of_zero and Limits.cokernel.π_zero_isIso.