Commit 2025-11-18 10:11 cd099a10

View on Github →

feat(Algebra): five lemma for vanishing of certain components (#31696) In this PR, we add five lemma for vanishing of certain components.

Estimated changes

Modified Mathlib/Algebra/FiveLemma.lean

added theorem AddMonoidHom.bijective_of_bijective_of_injective_of_left_exact

added theorem AddMonoidHom.bijective_of_surjective_of_bijective_of_right_exact

added theorem AddMonoidHom.injective_of_surjective_of_injective_of_right_exact

added theorem AddMonoidHom.surjective_of_surjective_of_injective_of_left_exact

added theorem LinearMap.bijective_of_bijective_of_injective_of_left_exact

added theorem LinearMap.bijective_of_surjective_of_bijective_of_right_exact

added theorem LinearMap.injective_of_surjective_of_injective_of_right_exact

added theorem LinearMap.surjective_of_surjective_of_injective_of_left_exact