mathlib3 documentation

category_theory.abelian.generator

A complete abelian category with enough injectives and a separator has an injective coseparator #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

Future work #

References #