def termℤ : Lean.ParserDescr

Equations

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

theorem Int.coe_nat_eq (n : ℕ) : ↑n = Int.ofNat n

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 = ↑(Nat.succ n)

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

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