Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2020-08-02 16:01 4588400f

View on Github →

chore(group_theory/*): refactor quotient groups to use bundled subgroups (#3321)

Estimated changes

modified def AddCommGroup.image.ι
modified def AddCommGroup.image
added theorem abelianization.hom_ext
modified theorem abelianization.lift.of
modified def abelianization.lift
modified def abelianization.of
modified def commutator
modified theorem eq_cosets_of_normal
modified theorem normal_iff_eq_cosets
modified theorem normal_of_eq_cosets
modified theorem right_coset_mem_right_coset
modified def free_group.map
modified theorem free_group.prod.unique
modified def free_group.prod
modified theorem free_group.to_group.unique
modified def free_group.to_group
modified def mul_action.comp_hom
modified def mul_action.stabilizer
modified theorem card_quotient_dvd_card
modified theorem card_subgroup_dvd_card
modified theorem card_trivial
modified theorem order_eq_card_gpowers
modified theorem powers_eq_gpowers
modified def quotient_group.lift
modified theorem quotient_group.lift_mk'
modified theorem quotient_group.lift_mk
modified def quotient_group.map
modified theorem monoid_hom.mem_ker
modified theorem subgroup.mem_bot
added theorem submonoid.mem_powers
added def submonoid.powers
modified def free_comm_ring.lift
modified theorem free_comm_ring.lift_comp_of
modified theorem quotient_group_saturate
deleted theorem is_submonoid.mem_nhds_one
added theorem submonoid.mem_nhds_one