[Merged by Bors] - feat: port CategoryTheory.Abelian.Pseudoelements

[int-y1]

---

[int-y1]

todo:

• problem with attribute [ext] on zero_morphism_ext and zero_morphism_ext'

[semorrison]

@int-y1, we've become more strict about the shape of ext lemmas, for better or worse, so the right thing to do here is remove them.

I've also switched all the pseudoZeros back to 0. In Lean 4 this instance has become safe as a global instance, because the coe_sort is replaced by Pseudoelement, so the instance is structural.

[semorrison]

If this looks good to you, please merge. Otherwise set back to awaiting-review or help-wanted as appropriate.

bors d+

[bors]

✌️ int-y1 can now approve this pull request. To approve and merge a pull request, simply reply with bors r+. More detailed instructions are available here.

[semorrison]

@int-y1, I started the next file, at #3882, please feel free to hack on it / adopt. :-)

[int-y1]

bors r+

[bors]

Pull request successfully merged into master.

Build succeeded!

The publicly hosted instance of bors-ng is deprecated and will go away soon.

If you want to self-host your own instance, instructions are here.
For more help, visit the forum.

If you want to switch to GitHub's built-in merge queue, visit their help page.

• Build
• Check all files imported
• Lint style