Polarization spanning of symmetric tensors ($\mathrm{span}\{a^{\otimes n}\}=(U^{\otimes n}{)}^{S_n}$)

Over a field of characteristic zero, degree-$n$ symmetric tensors are spanned by pure powers $a^{\otimes n}$. Inclusion-exclusion expands ${\sum }_{J\subseteq [n]}(-1{)}^{n-|J|}({\sum }_{j\in J}{a}_j{)}^{\otimes n}$ into the sum of all permutation orderings of $a_1\otimes \cdots \otimes a_n$. Every surviving term uses each of the $n$ labels once. This converts an invariant-tensor spanning problem into pure tensor powers.