mathlib3

9c2f6ebe - feat(category_theory/abelian/exact): `exact g.op f.op` (#12456)

feat(category_theory/abelian/exact): `exact g.op f.op` (#12456) This pr is about `exact g.op f.op` from `exact f g` in an abelian category; this pr is taken from liquid tensor experiment. I believe the original author is @adamtopaz.