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

Commit
3 years ago
feat(group_theory/subgroup/basic): If `H` is commutative, then `H ≤ H.centralizer` (#16718) If `H` is commutative, then `H ≤ H.centralizer`.
Author
Parents
Loading