Description: The norm of a nonzero element is a positive real. (Contributed by NM, 20-Nov-2007) (Revised by AV, 8-Oct-2021)