Commit 2024-05-24 03:47 aef75f7a

View on Github →

Feat(Algebra/Exact): Transport of exact sequences & the behavior under quotienting (#13126) Transport of exact sequences & the behavior under quotienting.

Estimated changes

Modified Mathlib/Algebra/Exact.lean

added theorem Function.Exact.apply_apply_eq_zero

added theorem Function.Exact.exact_mapQ_iff

added theorem Function.Exact.iff_of_ladder_linearEquiv

added theorem Function.Exact.of_comp_of_mem_range

added theorem Function.Exact.of_ladder_linearEquiv_of_exact

added theorem Function.Injective.comp_exact_iff_exact

deleted theorem Function.LinearMap.exact_iff

added theorem Function.Surjective.comp_exact_iff_exact

added theorem LinearEquiv.conj_exact_iff_exact

added theorem LinearMap.exact_iff

added theorem LinearMap.exact_of_comp_eq_zero_of_ker_le_range

added theorem LinearMap.exact_of_comp_of_mem_range