Commit 2024-04-20 06:50 8e052acc

View on Github →

chore: refactor to avoid importing Ring for Group topics (#11913) This is a far from a complete success at the PR title, but it makes a fair bit of progress, and then guards this with appropriate assert_not_exists Ring statements. It also breaks apart the Mathlib.GroupTheory.Subsemigroup.[Center|Centralizer] files, to pull the Set.center and Set.centralizer declarations into their own files not depending on Subsemigroup.

Estimated changes

added structure IsAddCentral
added structure IsMulCentral
added def Set.center
added theorem Set.center_eq_univ
added theorem Set.center_units_eq
added theorem Set.div_mem_center
added theorem Set.div_mem_center₀
added theorem Set.invOf_mem_center
added theorem Set.inv_mem_center
added theorem Set.inv_mem_center₀
added theorem Set.mem_center_iff
added theorem Set.mul_mem_center
added theorem Set.one_mem_center
added theorem Set.zero_mem_center
added def Set.centralizer
added theorem Set.centralizer_subset
added theorem Set.centralizer_univ
added theorem AddMonoidHom.coe_mul
added def AddMonoidHom.mul
added theorem AddMonoidHom.mul_apply
deleted theorem AddMonoidHom.coe_flip_mul
deleted theorem AddMonoidHom.coe_mul
deleted theorem AddMonoidHom.map_mul_iff
deleted def AddMonoidHom.mul
deleted theorem AddMonoidHom.mul_apply
deleted theorem RingHom.coe_pow
deleted theorem invOf_neg
deleted theorem invOf_two_add_invOf_two
deleted def invertibleNeg
deleted theorem one_sub_invOf_two
deleted theorem pos_of_invertible_cast
added theorem invOf_neg
added def invertibleNeg
added theorem one_sub_invOf_two
added theorem pos_of_invertible_cast
added theorem Set.add_mem_center
added theorem Set.intCast_mem_center
added theorem Set.natCast_mem_center
added theorem Set.neg_mem_center
added theorem Set.ofNat_mem_center
added theorem RingHom.coe_pow
deleted theorem CommGroup.center_eq_top
deleted theorem ConjClasses.mk_bijOn
deleted def Subgroup.center
deleted theorem Subgroup.centralizer_le
deleted theorem Subgroup.centralizer_univ
deleted theorem Subgroup.coe_center
deleted theorem Subgroup.le_centralizer
deleted theorem Subgroup.mem_center_iff
added theorem ConjClasses.mk_bijOn
added def Subgroup.center
added theorem Subgroup.coe_center
deleted structure IsAddCentral
deleted structure IsMulCentral
deleted theorem Semigroup.mem_center_iff
deleted theorem Set.add_mem_center
deleted def Set.center
deleted theorem Set.center_eq_univ
deleted theorem Set.center_units_eq
deleted theorem Set.center_units_subset
deleted theorem Set.div_mem_center
deleted theorem Set.div_mem_center₀
deleted theorem Set.intCast_mem_center
deleted theorem Set.invOf_mem_center
deleted theorem Set.inv_mem_center
deleted theorem Set.inv_mem_center₀
deleted theorem Set.mem_center_iff
deleted theorem Set.mul_mem_center
deleted theorem Set.natCast_mem_center
deleted theorem Set.neg_mem_center
deleted theorem Set.ofNat_mem_center
deleted theorem Set.one_mem_center
deleted theorem Set.subset_center_units
deleted theorem Set.units_inv_mem_center
deleted theorem Set.zero_mem_center
deleted theorem Set.add_mem_centralizer
deleted def Set.centralizer
deleted theorem Set.centralizer_eq_univ
deleted theorem Set.centralizer_subset
deleted theorem Set.centralizer_univ
deleted theorem Set.div_mem_centralizer
deleted theorem Set.inv_mem_centralizer
deleted theorem Set.mem_centralizer_iff
deleted theorem Set.mul_mem_centralizer
deleted theorem Set.neg_mem_centralizer
deleted theorem Set.one_mem_centralizer
deleted theorem Set.zero_mem_centralizer