Commit 2024-11-26 13:02 5ad34c03

feat(Algebra/Exact): iff lemmas (#19504) When we have a commutative diagram from a sequence of two maps to another, such that the left vertical map is surjective, the middle vertical map is bijective and the right vertical map is injective, then the upper row is exact iff the lower row is. This generalizes the case when all the three vertical maps are bijections. This PR introduces two new lemmas exact_iff_of_surjective_of_bijective_of_injective in the AddMonoidHom and LinearMap namespaces, and refactors the proofs of the all-bijections versions. This parallels the categorical lemma https://leanprover-community.github.io/mathlib4_docs/Mathlib/Algebra/Homology/ShortComplex/Exact.html#CategoryTheory.ShortComplex.exact_iff_of_epi_of_isIso_of_mono