Commit 2020-07-14 11:05 5f01b544

feat(category_theory/kernels): kernel_iso_of_eq (#3372) This provides two useful isomorphisms when working with abstract (co)kernels:

def kernel_zero_iso_source [has_kernel (0 : X ⟶ Y)] : kernel (0 : X ⟶ Y) ≅ X :=
def kernel_iso_of_eq {f g : X ⟶ Y} [has_kernel f] [has_kernel g] (h : f = g) : kernel f ≅ kernel g :=

and some associated simp lemmas.