Exact decimal remainder

IEEE 754-2019 §5.3.1 uses the nearest integer quotient, with even ties, regardless of the current rounding direction. Aligning the integer coefficients at the smaller quantum makes the computation exact, even for a quotient too large to represent as a decimal floating-point number. The result retains that preferred quantum. An exact zero keeps the dividend's sign (§6.3).

The default status has no underflow or inexact flag, including tiny exact remainders. Alternate exception handling is outside this pure result API.

def FloatLib.Floats.Formats.DecimalInterchange.Arithmetic.remainderRoundUp (a b : ℕ) : Bool

Whether the nearest integer quotient lies above the truncated quotient.

def FloatLib.Floats.Formats.DecimalInterchange.Arithmetic.remainderQuotient (a b : ℕ) : ℕ

Unbounded nearest-even quotient of two nonnegative integers.

def FloatLib.Floats.Formats.DecimalInterchange.Arithmetic.remainderCoefficient (a b : ℕ) : ℕ

Magnitude of the signed remainder on the common integer grid.

def FloatLib.Floats.Formats.DecimalInterchange.Arithmetic.remainderFinite (sx : Bool) (cx : ℕ) (qx : ℤ) (cy : ℕ) (qy : ℤ) : Datum

Exact remainder of finite operands on their common, preferred decimal grid.

def FloatLib.Floats.Formats.DecimalInterchange.Arithmetic.remainder (f : Format) : Datum → Datum → Outcome

IEEE remainder, independent of the rounding direction. Finite dividend/infinite divisor returns the dividend, including its cohort.