Equations
- termℤ = Lean.ParserDescr.node `termℤ 1024 (Lean.ParserDescr.symbol "ℤ")
The modulus of an integer by another as a natural. Uses the E-rounding convention.
Equations
- Int.natMod m n = Int.toNat (m % n)
Mathlib.Init.Data.Int.Basic
The modulus of an integer by another as a natural. Uses the E-rounding convention.