Commit 2024-10-28 17:42 4e5fa637

View on Github →

chore(Algebra/Group/Subgroup): split off Defs file (#18340) This PR splits off the definition of Subgroup and the Group instance into a new Defs file. Doing so required also moving the Semigroup instance on Subsemigroup and Monoid on Submonoid to the respective Defs file. So we needed to add one extra import: Algebra.Group.InjSurj. The imports and contents of that file are light enough in my opinion to make it worth it.

Estimated changes

deleted structure AddSubgroup.IsCommutative
deleted structure AddSubgroup.Normal
deleted structure AddSubgroup
deleted theorem InvMemClass.coe_inv
deleted structure Subgroup.IsCommutative
deleted theorem Subgroup.Normal.conj_mem'
deleted theorem Subgroup.Normal.mem_comm
deleted structure Subgroup.Normal
deleted theorem Subgroup.coeSubtype
deleted theorem Subgroup.coe_copy
deleted theorem Subgroup.coe_div
deleted theorem Subgroup.coe_inclusion
deleted theorem Subgroup.coe_inv
deleted theorem Subgroup.coe_mk
deleted theorem Subgroup.coe_mul
deleted theorem Subgroup.coe_nonempty
deleted theorem Subgroup.coe_one
deleted theorem Subgroup.coe_pow
deleted theorem Subgroup.coe_set_mk
deleted theorem Subgroup.coe_toSubmonoid
deleted theorem Subgroup.coe_zpow
deleted theorem Subgroup.copy_eq
deleted theorem Subgroup.ext
deleted def Subgroup.inclusion
deleted theorem Subgroup.inclusion_inj
deleted theorem Subgroup.le_normalizer
deleted theorem Subgroup.mem_carrier
deleted theorem Subgroup.mem_mk
deleted theorem Subgroup.mem_toSubmonoid
deleted theorem Subgroup.mk_eq_one
deleted theorem Subgroup.mk_le_mk
deleted def Subgroup.normalizer
deleted def Subgroup.ofDiv
deleted theorem Subgroup.toSubmonoid_eq
deleted theorem Subgroup.toSubmonoid_le
deleted theorem Subgroup.toSubmonoid_mono
deleted structure Subgroup
deleted theorem SubgroupClass.coeSubtype
deleted theorem SubgroupClass.coe_div
deleted theorem SubgroupClass.coe_pow
deleted theorem SubgroupClass.coe_zpow
deleted theorem div_mem
deleted theorem inv_mem_iff
deleted theorem mul_mem_cancel_left
deleted theorem mul_mem_cancel_right
deleted theorem zpow_mem
added structure AddSubgroup.IsCommutative
added structure AddSubgroup.Normal
added structure AddSubgroup
added theorem InvMemClass.coe_inv
added structure Subgroup.IsCommutative
added structure Subgroup.Normal
added theorem Subgroup.coeSubtype
added theorem Subgroup.coe_copy
added theorem Subgroup.coe_div
added theorem Subgroup.coe_inclusion
added theorem Subgroup.coe_inv
added theorem Subgroup.coe_mk
added theorem Subgroup.coe_mul
added theorem Subgroup.coe_nonempty
added theorem Subgroup.coe_one
added theorem Subgroup.coe_pow
added theorem Subgroup.coe_set_mk
added theorem Subgroup.coe_zpow
added theorem Subgroup.copy_eq
added theorem Subgroup.ext
added theorem Subgroup.inclusion_inj
added theorem Subgroup.le_normalizer
added theorem Subgroup.mem_carrier
added theorem Subgroup.mem_mk
added theorem Subgroup.mk_eq_one
added theorem Subgroup.mk_le_mk
added def Subgroup.ofDiv
added structure Subgroup
added theorem SubgroupClass.coe_div
added theorem SubgroupClass.coe_pow
added theorem SubgroupClass.coe_zpow
added theorem div_mem
added theorem inv_mem_iff
added theorem mul_mem_cancel_left
added theorem mul_mem_cancel_right
added theorem zpow_mem
added theorem OneMemClass.coe_eq_one
added theorem OneMemClass.coe_one
added theorem OneMemClass.one_def
added theorem Submonoid.coe_mul
added theorem Submonoid.coe_one
added theorem Submonoid.coe_subtype
added theorem Submonoid.mk_eq_one
added theorem Submonoid.mk_mul_mk
added theorem Submonoid.mul_def
added theorem Submonoid.one_def
added theorem SubmonoidClass.coe_pow
added theorem SubmonoidClass.mk_pow
deleted theorem OneMemClass.coe_eq_one
deleted theorem OneMemClass.coe_one
deleted theorem OneMemClass.one_def
deleted theorem Submonoid.coe_mul
deleted theorem Submonoid.coe_one
deleted theorem Submonoid.coe_subtype
deleted theorem Submonoid.mk_eq_one
deleted theorem Submonoid.mk_mul_mk
deleted theorem Submonoid.mul_def
deleted theorem Submonoid.one_def
deleted def Submonoid.subtype
deleted theorem SubmonoidClass.coe_pow
deleted theorem SubmonoidClass.mk_pow
added theorem MulMemClass.coe_mul
added theorem MulMemClass.mk_mul_mk
added theorem MulMemClass.mul_def
deleted theorem MulMemClass.coe_mul
deleted theorem MulMemClass.coe_subtype
deleted theorem MulMemClass.mk_mul_mk
deleted theorem MulMemClass.mul_def
deleted def MulMemClass.subtype