Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-08-09 09:08 b74907b6

View on Github →

feat(algebra/category/Group/epi_mono): (mono)epimorphisms and (in)surjections are the same in (Add)(Comm)Group (#15496)

Estimated changes

Modified src/algebra/category/Group/epi_mono.lean

added theorem AddGroup.epi_iff_range_eq_top

added theorem AddGroup.epi_iff_surjective

added theorem CommGroup.epi_iff_range_eq_top

added theorem CommGroup.epi_iff_surjective

added theorem CommGroup.ker_eq_bot_of_mono

added theorem CommGroup.mono_iff_injective

added theorem CommGroup.mono_iff_ker_eq_bot

added theorem CommGroup.range_eq_top_of_epi

added theorem monoid_hom.range_eq_top_of_cancel

Created src/algebra/category/Group/equivalence_Group_AddGroup.lean

added def AddCommGroup.to_CommGroup

added def AddGroup.to_Group

added def CommGroup.to_AddCommGroup

added def CommGroup_AddCommGroup_equivalence

added def Group.to_AddGroup

added def Group_AddGroup_equivalence

Modified src/algebra/hom/equiv.lean

added def add_equiv.additive_multiplicative

added def mul_equiv.multiplicative_additive