Commit 2026-01-08 11:26 34d89e32

View on Github →

chore(Algebra/Exact): refactor using to_additive (#33719) This PR adds Function.MulExact with the existing Function.Exact generated by to_additive. Supersedes #33587.

Estimated changes

Modified Mathlib/Algebra/Exact.lean

deleted theorem AddMonoidHom.exact_iff

deleted theorem AddMonoidHom.exact_iff_of_surjective_of_bijective_of_injective

deleted theorem AddMonoidHom.exact_of_comp_eq_zero_of_ker_le_range

deleted theorem AddMonoidHom.exact_of_comp_of_mem_range

deleted theorem Function.Exact.addMonoidHom_comp_eq_zero

deleted theorem Function.Exact.addMonoidHom_ker_eq

deleted theorem Function.Exact.apply_apply_eq_zero

deleted theorem Function.Exact.comp_eq_zero

deleted theorem Function.Exact.comp_injective

deleted theorem Function.Exact.iff_addMonoidHom_rangeRestrict

deleted theorem Function.Exact.iff_of_ladder_addEquiv

deleted theorem Function.Exact.iff_rangeFactorization

deleted theorem Function.Exact.of_comp_eq_zero_of_ker_in_range

deleted theorem Function.Exact.of_comp_of_mem_range

deleted theorem Function.Exact.of_ladder_addEquiv_of_exact'

deleted theorem Function.Exact.of_ladder_addEquiv_of_exact

deleted theorem Function.Exact.rangeFactorization

deleted def Function.Exact

added theorem Function.MulExact.apply_apply_eq_one

added theorem Function.MulExact.comp_eq_one

added theorem Function.MulExact.comp_injective

added theorem Function.MulExact.iff_monoidHom_rangeRestrict

added theorem Function.MulExact.iff_of_ladder_mulEquiv

added theorem Function.MulExact.iff_rangeFactorization

added theorem Function.MulExact.monoidHom_comp_eq_zero

added theorem Function.MulExact.monoidHom_ker_eq

added theorem Function.MulExact.of_comp_eq_one_of_ker_in_range

added theorem Function.MulExact.of_comp_of_mem_range

added theorem Function.MulExact.of_ladder_mulEquiv_of_mulExact'

added theorem Function.MulExact.of_ladder_mulEquiv_of_mulExact

added theorem Function.MulExact.rangeFactorization

added def Function.MulExact

added theorem MonoidHom.mulExact_iff

added theorem MonoidHom.mulExact_iff_of_surjective_of_bijective_of_injective

added theorem MonoidHom.mulExact_of_comp_eq_one_of_ker_le_range

added theorem MonoidHom.mulExact_of_comp_of_mem_range

Modified Mathlib/Algebra/FiveLemma.lean

deleted theorem AddMonoidHom.bijective_of_bijective_of_injective_of_left_exact

deleted theorem AddMonoidHom.bijective_of_surjective_of_bijective_of_bijective_of_injective

deleted theorem AddMonoidHom.bijective_of_surjective_of_bijective_of_right_exact

deleted theorem AddMonoidHom.injective_of_surjective_of_injective_of_injective

deleted theorem AddMonoidHom.injective_of_surjective_of_injective_of_right_exact

deleted theorem AddMonoidHom.surjective_of_surjective_of_injective_of_left_exact

deleted theorem AddMonoidHom.surjective_of_surjective_of_surjective_of_injective

added theorem MonoidHom.bijective_of_bijective_of_injective_of_left_exact

added theorem MonoidHom.bijective_of_surjective_of_bijective_of_bijective_of_injective

added theorem MonoidHom.bijective_of_surjective_of_bijective_of_right_exact

added theorem MonoidHom.injective_of_surjective_of_injective_of_injective

added theorem MonoidHom.injective_of_surjective_of_injective_of_right_exact

added theorem MonoidHom.surjective_of_surjective_of_injective_of_left_exact

added theorem MonoidHom.surjective_of_surjective_of_surjective_of_injective

Modified Mathlib/Tactic/Translate/ToAdditive.lean