Theorem Set.powersetCard.fixedPoints_ne_univ_of_faithfulSMul

Modification history

2026-04-28 15:42
Mathlib/GroupTheory/GroupAction/SubMulAction/Combination.lean
feat(GroupTheory/SpecificGroups/Alternating/Simple): simplicity of the alternating groups (#36524) …
Added Set.powersetCard.fixedPoints_ne_univ_of_faithfulSMulView on Github →