Commit 2024-10-29 13:45 8a2a5711

View on Github →

chore(GroupTheory/QuotientGroup): split off Defs file (#18348) The goal of this PR is to have a file with the definitions for the quotient of a group by a normal subgroup.

Estimated changes

deleted theorem QuotientGroup.coe_mk'
deleted def QuotientGroup.congr
deleted theorem QuotientGroup.congr_apply
deleted theorem QuotientGroup.congr_mk'
deleted theorem QuotientGroup.congr_mk
deleted theorem QuotientGroup.congr_refl
deleted theorem QuotientGroup.congr_symm
deleted theorem QuotientGroup.eq_one_iff
deleted theorem QuotientGroup.image_coe
deleted theorem QuotientGroup.ker_mk'
deleted def QuotientGroup.lift
deleted theorem QuotientGroup.lift_mk'
deleted theorem QuotientGroup.lift_mk
deleted def QuotientGroup.map
deleted theorem QuotientGroup.map_id
deleted theorem QuotientGroup.map_map
deleted theorem QuotientGroup.map_mk'
deleted theorem QuotientGroup.map_mk
deleted def QuotientGroup.mk'
deleted theorem QuotientGroup.mk'_apply
deleted theorem QuotientGroup.mk'_eq_mk'
deleted theorem QuotientGroup.mk_div
deleted theorem QuotientGroup.mk_inv
deleted theorem QuotientGroup.mk_mul
deleted theorem QuotientGroup.mk_one
deleted theorem QuotientGroup.mk_pow
deleted theorem QuotientGroup.mk_zpow
added theorem QuotientGroup.coe_mk'
added theorem QuotientGroup.congr_mk
added theorem QuotientGroup.ker_mk'
added theorem QuotientGroup.lift_mk'
added theorem QuotientGroup.lift_mk
added theorem QuotientGroup.map_id
added theorem QuotientGroup.map_map
added theorem QuotientGroup.map_mk'
added theorem QuotientGroup.map_mk
added theorem QuotientGroup.mk_div
added theorem QuotientGroup.mk_inv
added theorem QuotientGroup.mk_mul
added theorem QuotientGroup.mk_one
added theorem QuotientGroup.mk_pow
added theorem QuotientGroup.mk_zpow