6.6 The \(q\)-factorial generating function
In the polynomial ring \(\mathbb {Z}[q]\):
\[ [n]_q := 1 + q + q^2 + \dots + q^{n-1}, \qquad [n+1]_q! := [1]_q \cdot [2]_q \cdot \dots \cdot [n+1]_q. \]
Stanley EC1 §1.3.4 / Cor 1.3.10. For every \(n \in \mathbb {N}\),
\[ \sum _{\sigma \in \mathfrak {S}_{n+1}} q^{\mathrm{inv}(\sigma )} \; =\; [n+1]_q!. \]
Proved by induction on \(n\) using the value-based “insert \(\mathrm{ord}_{\max }\)” bijection \(\mathfrak {S}_{n+2} \simeq \mathfrak {S}_{n+1} \times \{ 0, \dots , n+1\} \) from \(\texttt{eulerian.v}\). The key step is \(\mathrm{inv}(\mathrm{insert\_ max\_ perm}(\tau , p)) = \mathrm{inv}(\tau ) + (n+1 - p)\).