ink

def termℤ : Lean.ParserDescr

Equations

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

ink

def Int.zero : ℤ

The number 0 : ℤ, as a standalone definition.

Equations

• Int.zero = Int.ofNat 0

ink

def Int.one : ℤ

The number 1 : ℤ, as a standalone definition.

Equations

• Int.one = Int.ofNat 1

ink

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

ink

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

ink

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

ink

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

ink

theorem Int.eq_zero_of_natAbs_eq_zero {a : ℤ} : Int.natAbs a = 0 → a = 0

ink

theorem Int.natAbs_pos_of_ne_zero {a : ℤ} (h : a ≠ 0) : 0 < Int.natAbs a

ink

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)