Theorem Subgroup.mem_centralizer_iff_commutator_eq_one'

Modification history

2026-04-07 10:05
Mathlib/GroupTheory/Subgroup/Centralizer.lean
feat(GroupTheory/Subgroup): basic API for set normalizers (#36760)
Added Subgroup.mem_centralizer_iff_commutator_eq_one'View on Github →