OAI/CategoryTheory/Limits/KernelRetraction.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

A nonzero kernel morphism obstructs a retraction.

  1. theorem OAI.KernelObstruction.no_retraction_of_nonzero_kernel line 11