Steinberg relation for the Galois symbol

Let $F$ be a field of characteristic different from $2$, let $F^{\mathrm{sep}}$ be a separable closure and $G_F=\operatorname{Gal}(F^{\mathrm{sep}}/F)$. For $a\in F^\times$ let $\chi_a:G_F\to\mathbb{Z}/2$ be the Kummer character ($\chi_a(\sigma)=0$ iff $\sigma$ fixes a chosen square root of $a$). For $a=(a_1,\dots,a_n)\in(F^\times)^n$, the Galois symbol $\mathrm{gs}(a_1,\dots,a_n)\in H^n(F,\mathbb{Z}/2)$ is the cup product $\chi_{a_1}\cup\cdots\cup\chi_{a_n}$ in continuous Galois cohomology (with $\mathrm{gs}()=1\in H^0$).

Then the Galois symbol satisfies the Steinberg relation: if two adjacent entries satisfy $a_i+a_{i+1}=1$, then

In degree $2$ this is Tate's relation $\chi_a\cup\chi_{1-a}=0$; in general it follows from it by the associativity of the cup product. Together with multiplicativity in each slot, it shows that the Galois symbol factors through Milnor K-theory.

Formalization Note Adjacency is expressed by indices $i,j$ with $i+1=j$ (as natural numbers), matching the definition of the Steinberg subgroup in MilnorConjecture_MilnorK.