mathlib3
8c64be0b - chore(category_theory/abelian): Moved more stuff into `pseudoelement` locale (#11621)

Commit

3 years ago

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

Author

erdOne

Parents