mathlib3 documentation

category_theory.abelian.opposite

The opposite of an abelian category is abelian. #

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

The opposite of the image of f is the image of f.op.

Equations