Theorem IsPGroup.smul_mul_inv_trivial_or_surjective

Modification history

2025-01-13 10:02
Mathlib/GroupTheory/SpecificGroups/ZGroup.lean
feat(GroupTheory/SpecificGroups/ZGroup): Commutator subgroup of a Z-group is a Hall subgroup (#20694) …
Added IsPGroup.smul_mul_inv_trivial_or_surjectiveView on Github →