Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-08-31 10:54 ab967d23

View on Github →

feat(group_theory/submonoid): center of a submonoid (#8921) This adds set.center, submonoid.center, subsemiring.center, and subring.center, to complement the existing subgroup.center. This ran into a timeout, so had to squeeze some simps in an unrelated file.

Estimated changes

added theorem subgroup.coe_center
added theorem set.add_mem_center
added def set.center
added theorem set.center_eq_univ
added theorem set.center_units_eq
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.neg_mem_center
added theorem set.one_mem_center
added theorem set.zero_mem_center
added def submonoid.center
added theorem submonoid.coe_center
added def subring.center
added theorem subring.center_eq_top
added theorem subring.coe_center
added theorem subring.mem_center_iff
added theorem subsemiring.coe_center