Theorem Set.powersetCard.isPreprimitive_perm

Modification history

2026-02-02 08:05
Mathlib/GroupTheory/GroupAction/SubMulAction/Combination.lean
feat(GroupTheory/GroupAction/SubMulAction/Combination): primitivity of the permutation action. (#34307) …
Added Set.powersetCard.isPreprimitive_permView on Github →