Revision #3196 → #3701 · back to history
fcb5ed94b23b| Field | From #3196 | To #3701 |
|---|---|---|
| mathlib.decl | commutator_inf_eq_focalSubgroup | Subgroup.commutator_inf_eq_focalSubgroup |
| note | `commutator_inf_eq_focalSubgroup` in `Mathlib.GroupTheory.Focal` is the Focal Subgroup Theorem: `commutator G ⊓ P = P.focalSubgroup`. | `Subgroup.commutator_inf_eq_focalSubgroup` in `Mathlib.GroupTheory.Focal` is the Focal Subgroup Theorem: `commutator G ⊓ P = P.focalSubgroup`. |
8be445cb8795