Commit 2023-06-09 14:50 cc67cd75

View on Github →

chore(*/centralizer): add forgotten to_additives (#19168) I forgot these in #18861. These are already in the forward-port PR, leanprover-community/mathlib4#4896.

Estimated changes

Modified src/group_theory/subgroup/basic.lean

modified theorem subgroup.center_le_centralizer

modified theorem subgroup.centralizer_eq_top_iff_subset

Modified src/group_theory/submonoid/centralizer.lean

modified theorem submonoid.center_le_centralizer

modified theorem submonoid.centralizer_eq_top_iff_subset

Modified src/group_theory/subsemigroup/centralizer.lean

modified theorem set.centralizer_eq_top_iff_subset

modified theorem subsemigroup.centralizer_eq_top_iff_subset