\Z in VS Code) are an inductive type with two constructors —
of_nat (which takes a natural number
n to the associated integer
neg_succ_of_nat (which takes
n to the integer
There are around 30 theorems about integers in core lean and around 200 more in mathlib. Here are some examples of theorems in core Lean:
open int example : (6:ℤ) = of_nat (6:ℕ) := rfl example : (-6:ℤ) = neg_succ_of_nat (5:ℕ) := rfl example : -[1+5] = neg_succ_of_nat 5 := rfl -- + - * all defined. -- Compability of these with the corresponding operators -- on naturals needs to be checked -- Explicit coercion from ℕ to ℤwith of_nat example (m n : ℕ) : of_nat (m * n) = of_nat m * of_nat n := of_nat_mul m n -- Automatic coercion with an up-arrow. This lemma is protected -- so we need to write "int" even though we opened int. example (m n : ℕ) : (↑(m * n) : ℤ) = ↑m * ↑n := int.coe_nat_mul m n -- injectivity of coercion example (m n : ℕ) : (↑m : ℤ) = (↑n : ℤ) → m = n := int.coe_nat_inj -- nat_abs is the absolute value from ℤ to ℕ example : nat_abs (-6) = 6 := rfl example (a : ℤ) : ↑(nat_abs a * nat_abs a) = a * a := nat_abs_mul_self -- Three ways to do division and remainder! example : int.mod (-5) (-2) = 1 := rfl example : int.div (-5) (-2) = 3 := rfl -- try fdiv/fmod and quot/rem for the other conventions. -- ℤ is a commutative ring: example : comm_ring ℤ := by apply_instance -- so anything you can do with commutative rings you can do in ℤ. example (a : ℤ) : a * 0 = 0 := mul_zero a
And here are a few examples of what one can do using mathlib.
import data.int.basic import data.nat.gcd open int example (m n : ℕ) : (↑(m * n) : ℤ) = ↑m * ↑n := by simp -- wouldn't work without the import -- but note rfl works, -- division is defined on all of ℤ because type theory. example (a : ℤ) : a / 0 = 0 := int.div_zero a -- junk theorem example (a b : ℤ) : a / (-b) = -(a / b) := int.div_neg a b -- junk for b=0. example (a b c : ℤ) : c ≠ 0 → (a + b * c) / c = a / c + b := int.add_mul_div_right a b example (a b c d : ℤ) : (a - c) % d = (b - c) % d ↔ a % d = b % d := mod_sub_cancel_right c example (a b : ℤ) (α : Type) [ring α] : (((a + b) : ℤ) : α) = (a : α) + (b : α) := cast_add a b -- extended gcd's are actually in mathlib's nat section open nat example (m n : ℕ) : int.gcd m n = m * (gcd_a m n) + n * (gcd_b m n) := gcd_eq_gcd_ab
The general principle for finding these theorems is to understand the naming convention for mathlib lemmas and to use the search functionality of your IDE (VS Code or emacs) to find the lemma you want.