Finiteness of the zero set up to a height

The non-trivial zeros with imaginary part in (0, T] form a finite set, and each has positive multiplicity. This is what lets the rescaled zeros be a finite multiset, which every statement of the key proposition requires.

It is discharged from Mathlib's IsCompact.inter_riemannZetaZeros_finite, since the region is bounded.

theorem ZetaZeros.nontrivialZeros_finite (T : ℝ) : (nontrivialZeros T).Finite

The zero set up to a height is finite.