Documentation

Mathlib.CategoryTheory.Abelian.Injective

Injective objects in abelian categories #

The preadditive Yoneda functor on J preserves homology if J is injective.

Equations