Maths in Lean : integers

The integers (written \Z in VS Code) are an inductive type with two constructors — of_nat (which takes a natural number n to the associated integer (n:ℤ)) and neg_succ_of_nat (which takes n to the integer -1-n).

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.

Advertisements