The sup norm of an integer vector

The norm on ℤ is the restriction of the norm on ℝ (Int.norm_cast_real). Coordinatewise, the sup norm of an integer vector z : ι → ℤ is the sup norm of the real vector with the same coordinates (TauCeti.pi_norm_intCast_real).

theorem TauCeti.pi_norm_intCast_real {ι : Type u_1} [Fintype ι] (z : ι → ℤ) : ‖fun (i : ι) => ↑(z i)‖ = ‖z‖

The sup norm of an integer vector is the sup norm of its cast to a real vector.