[Numpy-discussion] Rounding the decimal part of a real number