@[deprecated Int.natAbs_eq_zero]
@[deprecated Int.natAbs_pos]
The modulus of an integer by another as a natural. Uses the E-rounding convention.
Mathlib.Init.Data.Int.Basic
The modulus of an integer by another as a natural. Uses the E-rounding convention.