Basic norm bounds for RCLike fields

Main results

• RCLike.norm_le_abs_re_add_abs_im: ‖z‖ ≤ |re z| + |im z|, the RCLike counterpart of Complex.norm_le_abs_re_add_abs_im.

theorem RCLike.norm_le_abs_re_add_abs_im {K : Type u_1} [RCLike K] (z : K) : ‖z‖ ≤ |re z| + |im z|

The norm of a scalar is at most the sum of the absolute values of its real and imaginary parts.