Commit 2022-12-31 22:14 f5db9bfc

View on Github →

feat: port GroupTheory.Subsemigroup.Center (#1278)

Estimated changes

Modified Mathlib.lean

Created Mathlib/GroupTheory/Subsemigroup/Center.lean

added def Set.Center

added theorem Set.add_mem_center

added theorem Set.center_eq_univ

added theorem Set.center_units_eq

added theorem Set.center_units_subset

added theorem Set.div_mem_center

added theorem Set.div_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.neg_mem_center

added theorem Set.one_mem_center

added theorem Set.subset_center_units

added theorem Set.zero_mem_center

added def Subsemigroup.Center

added theorem Subsemigroup.center_eq_top

added theorem Subsemigroup.mem_center_iff