Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-12-10 21:59 a12fc705

View on Github →

feat(logic/function/basic): surjective function is an epimorphism (#10691)

Move proofs about surjective/injective and epi/mono to logic.function.basic (formulated in terms of injectivity of composition), make them universe polymorphic.
drop forall_iff_forall_surj, use function.surjective.forall instead.

Estimated changes

Modified src/algebra/group/hom.lean

Modified src/algebra/ring/basic.lean

Modified src/category_theory/types.lean

Modified src/logic/basic.lean

deleted theorem forall_iff_forall_surj

Modified src/logic/function/basic.lean

modified theorem function.bijective.comp_left

added theorem function.bijective.comp_right

added theorem function.injective.surjective_comp_right'

added theorem function.injective.surjective_comp_right

modified theorem function.surjective.comp_left

added theorem function.surjective.injective_comp_right

modified theorem function.surjective.of_comp_iff'

added theorem function.surjective_of_right_cancellable_Prop