All matrices and vectors in this post have entries in the field $\mathbb{F}_2$.
Fix some $n \geq 1$. For an $n \times n$ matrix $X$, write $X_0$ for the column vector whose entries are the diagonal entries in $X$. The following curious fact arose in a paper I am writing:
Fact: Let $X$ be a symmetric $n \times n$ matrix and let $A$ be an arbitrary $n \times n$ matrix. Then $(AXA^t)_0 = A (X_0)$. Here $A (X_0)$ means that we are multiplying the column vector $X_0$ by $A$.
This is easy enough to prove in a grungy way, but to me it basically comes out of nowhere. Does anyone know a conceptual reason for it? Or perhaps a bigger picture in which it sits?