Commit 2023-05-10 11:05 94759f87

View on Github →

feat: port Algebra.Category.GroupCat.EpiMono (#3871)

Estimated changes

Modified Mathlib.lean

Created Mathlib/Algebra/Category/GroupCat/EpiMono.lean

added theorem AddGroupCat.epi_iff_range_eq_top

added theorem AddGroupCat.epi_iff_surjective

added theorem CommGroupCat.epi_iff_range_eq_top

added theorem CommGroupCat.epi_iff_surjective

added theorem CommGroupCat.ker_eq_bot_of_mono

added theorem CommGroupCat.mono_iff_injective

added theorem CommGroupCat.mono_iff_ker_eq_bot

added theorem CommGroupCat.range_eq_top_of_epi

added inductive GroupCat.SurjectiveOfEpiAuxs.XWithInfinity

added theorem GroupCat.SurjectiveOfEpiAuxs.agree

added theorem GroupCat.SurjectiveOfEpiAuxs.comp_eq

added theorem GroupCat.SurjectiveOfEpiAuxs.fromCoset_eq_of_mem_range

added theorem GroupCat.SurjectiveOfEpiAuxs.fromCoset_ne_of_nin_range

added def GroupCat.SurjectiveOfEpiAuxs.g

added theorem GroupCat.SurjectiveOfEpiAuxs.g_apply_fromCoset

added theorem GroupCat.SurjectiveOfEpiAuxs.g_apply_infinity

added theorem GroupCat.SurjectiveOfEpiAuxs.g_ne_h

added def GroupCat.SurjectiveOfEpiAuxs.h

added theorem GroupCat.SurjectiveOfEpiAuxs.h_apply_fromCoset'

added theorem GroupCat.SurjectiveOfEpiAuxs.h_apply_fromCoset

added theorem GroupCat.SurjectiveOfEpiAuxs.h_apply_fromCoset_nin_range

added theorem GroupCat.SurjectiveOfEpiAuxs.h_apply_infinity

added theorem GroupCat.SurjectiveOfEpiAuxs.mul_smul

added theorem GroupCat.SurjectiveOfEpiAuxs.one_smul

added theorem GroupCat.SurjectiveOfEpiAuxs.τ_apply_fromCoset'

added theorem GroupCat.SurjectiveOfEpiAuxs.τ_apply_fromCoset

added theorem GroupCat.SurjectiveOfEpiAuxs.τ_apply_infinity

added theorem GroupCat.SurjectiveOfEpiAuxs.τ_symm_apply_fromCoset

added theorem GroupCat.SurjectiveOfEpiAuxs.τ_symm_apply_infinity

added theorem GroupCat.epi_iff_range_eq_top

added theorem GroupCat.epi_iff_surjective

added theorem GroupCat.ker_eq_bot_of_mono

added theorem GroupCat.mono_iff_injective

added theorem GroupCat.mono_iff_ker_eq_bot

added theorem GroupCat.surjective_of_epi

added theorem MonoidHom.ker_eq_bot_of_cancel

added theorem MonoidHom.range_eq_top_of_cancel