Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-01-24 07:24 8c64be0b

View on Github →

chore(category_theory/abelian): Moved more stuff into pseudoelement locale (#11621) The ext lemma triggers unwantedly in lots of places.

Estimated changes

Modified src/category_theory/abelian/diagram_lemmas/four.lean

Modified src/category_theory/abelian/pseudoelements.lean

modified theorem category_theory.abelian.pseudoelement.zero_morphism_ext'

modified theorem category_theory.abelian.pseudoelement.zero_morphism_ext