Solution (source code)

= Solution

Identify the real span of the <roots> with its dual using the invariant <inner product>, and put $\alpha^\vee=2\alpha/(\alpha,\alpha)$. The <weight lattice> is
$$
\boxed{\Lambda_W=\{\lambda:\langle\lambda,\alpha^\vee\rangle\in\mathbb Z\text{ for every root }\alpha\}.}
$$
The <Weyl group> is generated by the <root reflections> $s_\alpha$. Each reflection permutes the finite set of <roots> and preserves their lengths, hence also permutes their coroots. Thus, for $\lambda\in\Lambda_W$,
$$
\langle s_\alpha\lambda,\beta^\vee\rangle=\langle\lambda,(s_\alpha\beta)^\vee\rangle\in\mathbb Z.
$$
Every generating reflection therefore maps the <weight lattice> to itself, and so does every product. Since the inverse product has the same property, \b[every Weyl-group element acts bijectively on $\Lambda_W$]. The <roots> span the ambient space, so the action on the finite <root> set is faithful; in particular the <Weyl group> is finite.