∀ (G : Type u_1) [inst : Group G] (α : Type u_2) [inst_1 : MulAction G α] (n : ℕ) [inst_2 : DecidableEq α],
  Set.powersetCard.mulActionHom_of_embedding G α n = { toFun := Set.powersetCard.ofFinEmb n α, map_smul' := ⋯ }