Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-05-04 07:50 455393d3

View on Github →

refactor(group_theory/{submonoid, subsemigroup}/{center, centralizer}): move set.center and set.centralizer into subsemigroup (#13903) This moves set.center and set.centralizer (the center and centralizers for a magma) into group_theory/subsemigroup/{center, centralizer} so that we can define the center and centralizers for semigroups in #13627.

Estimated changes

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.inv_mem_center
deleted theorem set.inv_mem_center₀
deleted theorem set.mem_center_iff
deleted theorem set.mul_mem_center
deleted theorem set.neg_mem_center
deleted theorem set.one_mem_center
deleted theorem set.subset_center_units
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
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.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.zero_mem_center
added def set.centralizer
added theorem set.centralizer_subset
added theorem set.centralizer_univ