Finite symplectic group order (source code)

= Finite symplectic group order
{title2=$q^{m^2}\prod_{i=1}^m(q^{2i}-1)$}

Counting successive symplectic pairs gives
$$
|\operatorname{Sp}_{2m}(q)|=q^{m^2}\prod_{i=1}^m(q^{2i}-1).
$$
For each nonzero first vector there are $q^{2m-1}$ partners with pairing one, after which its nondegenerate plane splits off. The exact defining-characteristic part is $q^{m^2}$, realized by an upper symplectic unitriangular subgroup.