Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-02-28 02:34 f3a04eda

View on Github →

feat(group_theory/subgroup/basic): Centralizer subgroup (#11946) This PR defines the centralizer subgroup, and provides a few basic lemmas.

Estimated changes

Modified src/group_theory/subgroup/basic.lean

added def subgroup.centralizer

added theorem subgroup.centralizer_top

added theorem subgroup.mem_centralizer_iff

added theorem subgroup.mem_centralizer_iff_commutator_eq_one

Created src/group_theory/submonoid/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 submonoid.centralizer

added theorem submonoid.centralizer_subset

added theorem submonoid.centralizer_univ

added theorem submonoid.coe_centralizer

added theorem submonoid.mem_centralizer_iff