Commit 2024-07-10 17:26 c6cc81dc

View on Github →

chore: Merge Algebra.Group.Centralizer into Algebra.Group.Center (#13034)

Estimated changes

modified theorem Set.center_eq_univ
added def Set.centralizer
added theorem Set.centralizer_subset
added theorem Set.centralizer_univ
modified theorem Set.div_mem_center
modified theorem Set.invOf_mem_center
modified theorem Set.inv_mem_center
modified theorem Set.mul_mem_center
modified theorem Set.one_mem_center
modified theorem Set.subset_center_units
modified theorem Set.units_inv_mem_center
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.one_mem_centralizer
modified theorem Set.center_units_eq
modified theorem Set.center_units_subset
modified theorem Set.div_mem_centralizer₀
modified theorem Set.inv_mem_centralizer₀
modified theorem Set.zero_mem_center
modified theorem Set.zero_mem_centralizer