def termℤ : Lean.ParserDescr

Equations

• termℤ = Lean.ParserDescr.node `termℤ 1024 (Lean.ParserDescr.symbol "ℤ")

theorem Int.ofNat_add_out (m : ℕ) (n : ℕ) : ↑m + ↑n = ↑(m + n)

theorem Int.ofNat_mul_out (m : ℕ) (n : ℕ) : ↑m * ↑n = ↑(m * n)

theorem Int.ofNat_add_one_out (n : ℕ) : ↑n + 1 = ↑n.succ

theorem Int.neg_eq_neg {a : ℤ} {b : ℤ} (h : -a = -b) : a = b

def Int.natMod (m : ℤ) (n : ℤ) : ℕ

The modulus of an integer by another as a natural. Uses the E-rounding convention.

Equations

• m.natMod n = (m % n).toNat