Commit 2025-05-01 09:09 9e67d115

View on Github →

feat(Algebra/Exact): add Function.Exact.[iff_]rangeFactorization etc (#23446) Two maps f : M → N and g : N → P are exact if and only if the induced maps Set.range f → N → Set.range g are exact. Same for AddMonoidHom and LinearMap.

Estimated changes

Modified Mathlib/Algebra/Exact.lean

added theorem Function.Exact.iff_addMonoidHom_rangeRestrict

added theorem Function.Exact.iff_linearMap_rangeRestrict

modified theorem Function.Exact.iff_of_ladder_linearEquiv

added theorem Function.Exact.iff_rangeFactorization

modified theorem Function.Exact.of_ladder_linearEquiv_of_exact

added theorem Function.Exact.rangeFactorization