Commit 2026-02-12 04:48 706fd956

chore: separate basic API for Set.powersetCard (#35068) This moves the basic API for Set.powersetCard in file GroupTheory.GroupAction.SubMulAction.Combination.lean that doesn't depend on a MulAction to a new file Data.Set.PowersetCard.lean.

• Moves definitions not dependent on MulAction to new file
• ofFinEmb is set version of mulActionHom_of_embedding
• ofSingleton is set version of mulActionHom_singleton
• compl is now a set version
• Rename compl to mulActionHom_compl (and related theorems)
• map n f is the map on powersetCard n induced by an injective map f