[Merged by Bors] - feat: exactness of short complexes

[joelriou]

This PR introduces the definition of a proposition S.Exact when S is a short complex.

---

[jcommelin]

Under suitable assumptions, this new definition of exactness is equivalent to the existing one in mathlib. I understand that you plan to phase out the old definition. But in the mean time, I think it is good to provide a "glue" lemma that shows that the two are equivalent.

[joelriou]

Thanks for the suggestions! I shall include a comparison lemma with the current Exact f g under suitable assumptions, but I need slightly more basic API (one or two PR on this file) before I can do this.

[jcommelin]

Thanks 🎉

bors merge

[bors]

Build failed (retrying...):

• Build

[bors]

Build failed (retrying...):

• Build

[bors]

Build failed:

• Build

[joelriou]

bors retry

[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