Mathlib v3 is deprecated. Go to Mathlib v4

Theorem subgroup.le_centralizer_iff_is_commutative

Modification history

2023-07-24 08:57

src/group_theory/subgroup/basic.lean

fix(group_theory/subgroup/basic): generalize `centralizer` from `subgroup G` to `set G` (#18965) …

Modified subgroup.le_centralizer_iff_is_commutative View on Github →

2022-10-01 18:32

src/group_theory/subgroup/basic.lean

feat(group_theory/subgroup/basic): If `H` is commutative, then `H ≤ H.centralizer` (#16718) …

Added subgroup.le_centralizer_iff_is_commutative View on Github →