Commit 2023-01-02 20:39 3ad51518

View on Github →

feat: port GroupTheory.Subsemigroup.Centralizer (#1286) I commented out the assertion in the bottom since we don't have it as of now and it is not relevant to the port itself.

Estimated changes

Modified Mathlib.lean

Created Mathlib/GroupTheory/Subsemigroup/Centralizer.lean

added theorem Set.add_mem_centralizer

added def Set.centralizer

added theorem Set.centralizer_eq_univ

added theorem Set.centralizer_subset

added theorem Set.centralizer_univ

added theorem Set.div_mem_centralizer

added theorem Set.div_mem_centralizer₀

added theorem Set.inv_mem_centralizer

added theorem Set.inv_mem_centralizer₀

added theorem Set.mem_centralizer_iff

added theorem Set.mul_mem_centralizer

added theorem Set.neg_mem_centralizer

added theorem Set.one_mem_centralizer

added theorem Set.zero_mem_centralizer

added def Subsemigroup.centralizer

added theorem Subsemigroup.centralizer_le

added theorem Subsemigroup.centralizer_univ

added theorem Subsemigroup.coe_centralizer

added theorem Subsemigroup.mem_centralizer_iff