Theorem Subgroup.transferFocal_surjective

Modification history

2026-02-26 14:02

Mathlib/GroupTheory/Focal.lean

feat(GroupTheory/Focal): add focal subgroup theorem (#34380) …

Added Subgroup.transferFocal_surjective View on Github →