Commit 2023-01-03 22:36 f6c80f83

View on Github →

feat: port GroupTheory.Submonoid.Center (#1315) Also includes fixes in other files as well (Set.Center to Set.center and a few more like that).

Estimated changes

added def Submonoid.center
added theorem Submonoid.coe_center
deleted def Set.Center
modified theorem Set.add_mem_center
added def Set.center
modified theorem Set.center_eq_univ
modified theorem Set.center_units_eq
modified theorem Set.center_units_subset
modified theorem Set.div_mem_center
modified theorem Set.div_mem_center₀
modified theorem Set.inv_mem_center
modified theorem Set.inv_mem_center₀
modified theorem Set.mem_center_iff
modified theorem Set.mul_mem_center
modified theorem Set.neg_mem_center
modified theorem Set.one_mem_center
modified theorem Set.subset_center_units
modified theorem Set.zero_mem_center
deleted def Subsemigroup.Center
modified theorem Subsemigroup.center_eq_top
modified theorem Subsemigroup.mem_center_iff
modified theorem Set.centralizer_univ