Theorem Subgroup.ker_restrict_transferFocal_eq_focalSubgroupOf

Modification history

2026-02-26 14:02
Mathlib/GroupTheory/Focal.lean
feat(GroupTheory/Focal): add focal subgroup theorem (#34380) …
Added Subgroup.ker_restrict_transferFocal_eq_focalSubgroupOfView on Github →