mathlib documentation

data.int.basic

Basic instances on the integers #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. https://github.com/leanprover-community/mathlib4/pull/584 Any changes to this file require a corresponding PR to mathlib4.

This file contains:

instances on ℤ. The stronger one is int.comm_ring. See data/int/defs/order for int.linear_ordered_comm_ring.
basic lemmas about the integers, but which do not use the ordered algebra hierarchy.

@[protected, instance]

def int.inhabited :

Equations

int.inhabited = {default := int.zero}

@[protected, instance]

def int.nontrivial :

@[protected, instance]

def int.comm_ring :

Equations

int.comm_ring = {add := int.add, add_assoc := int.add_assoc, zero := int.zero, zero_add := int.zero_add, add_zero := int.add_zero, nsmul := ring.nsmul._default int.zero int.add int.zero_add int.add_zero, nsmul_zero' := int.comm_ring._proof_1, nsmul_succ' := int.comm_ring._proof_2, neg := int.neg, sub := int.sub, sub_eq_add_neg := int.comm_ring._proof_3, zsmul := has_mul.mul int.has_mul, zsmul_zero' := int.zero_mul, zsmul_succ' := int.comm_ring._proof_4, zsmul_neg' := int.comm_ring._proof_5, add_left_neg := int.add_left_neg, add_comm := int.add_comm, int_cast := λ (n : ℤ), n, nat_cast := int.of_nat, one := int.one, nat_cast_zero := int.comm_ring._proof_6, nat_cast_succ := int.comm_ring._proof_7, int_cast_of_nat := int.comm_ring._proof_8, int_cast_neg_succ_of_nat := int.comm_ring._proof_9, mul := int.mul, mul_assoc := int.mul_assoc, one_mul := int.one_mul, mul_one := int.mul_one, npow := ring.npow._default int.one int.mul int.one_mul int.mul_one, npow_zero' := int.comm_ring._proof_10, npow_succ' := int.comm_ring._proof_11, left_distrib := int.distrib_left, right_distrib := int.distrib_right, mul_comm := int.mul_comm}

Extra instances to short-circuit type class resolution #

These also prevent non-computable instances like int.normed_comm_ring being used to construct these instances non-computably.

@[protected, instance]

def int.add_comm_monoid :

add_comm_monoid ℤ

Equations

int.add_comm_monoid = add_comm_group.to_add_comm_monoid ℤ

@[protected, instance]

def int.add_monoid :

Equations

int.add_monoid = add_monoid_with_one.to_add_monoid ℤ

@[protected, instance]

def int.monoid :

Equations

int.monoid = ring.to_monoid ℤ

@[protected, instance]

def int.comm_monoid :

comm_monoid ℤ

Equations

int.comm_monoid = comm_ring.to_comm_monoid ℤ

@[protected, instance]

def int.comm_semigroup :

comm_semigroup ℤ

Equations

int.comm_semigroup = non_unital_comm_ring.to_comm_semigroup ℤ

@[protected, instance]

def int.semigroup :

Equations

int.semigroup = semigroup_with_zero.to_semigroup ℤ

@[protected, instance]

def int.add_comm_group :

add_comm_group ℤ

Equations

int.add_comm_group = non_unital_non_assoc_ring.to_add_comm_group ℤ

@[protected, instance]

def int.add_group :

Equations

int.add_group = add_group_with_one.to_add_group ℤ

@[protected, instance]

def int.add_comm_semigroup :

add_comm_semigroup ℤ

Equations

int.add_comm_semigroup = add_comm_monoid.to_add_comm_semigroup ℤ

@[protected, instance]

def int.add_semigroup :

add_semigroup ℤ

Equations

int.add_semigroup = add_monoid.to_add_semigroup ℤ

@[protected, instance]

def int.comm_semiring :

comm_semiring ℤ

Equations

int.comm_semiring = comm_ring.to_comm_semiring

@[protected, instance]

def int.semiring :

Equations

int.semiring = ring.to_semiring

@[protected, instance]

def int.ring :

Equations

int.ring = comm_ring.to_ring ℤ

@[protected, instance]

def int.distrib :

Equations

int.distrib = ring.to_distrib ℤ

@[simp]

theorem int.add_neg_one (i : ℤ) :

i + -1 = i - 1

@[simp]

theorem int.default_eq_zero :

inhabited.default = 0

@[protected, instance]

meta def int.has_to_format :

has_to_format ℤ

@[protected, instance]

meta def int.reflect :

has_reflect ℤ

@[simp]

theorem int.add_def {a b : ℤ} :

a.add b = a + b

@[simp]

theorem int.mul_def {a b : ℤ} :

a.mul b = a * b

@[simp]

theorem int.neg_succ_not_nonneg (n : ℕ) :

0 ≤ -[1+ n] ↔ false

@[simp]

theorem int.neg_succ_not_pos (n : ℕ) :

0 < -[1+ n] ↔ false

@[simp]

theorem int.neg_succ_sub_one (n : ℕ) :

-[1+ n] - 1 = -[1+ n + 1]

@[simp]

theorem int.coe_nat_mul_neg_succ (m n : ℕ) :

↑m * -[1+ n] = -(↑m * ↑(n.succ))

@[simp]

theorem int.neg_succ_mul_coe_nat (m n : ℕ) :

-[1+ m] * ↑n = -(↑(m.succ) * ↑n)

@[simp]

theorem int.neg_succ_mul_neg_succ (m n : ℕ) :

-[1+ m] * -[1+ n] = ↑(m.succ) * ↑(n.succ)

theorem int.coe_nat_le {m n : ℕ} :

↑m ≤ ↑n ↔ m ≤ n

theorem int.coe_nat_lt {m n : ℕ} :

↑m < ↑n ↔ m < n

theorem int.coe_nat_inj' {m n : ℕ} :

↑m = ↑n ↔ m = n

theorem int.coe_nat_strict_mono :

strict_mono coe

theorem int.coe_nat_nonneg (n : ℕ) :

@[simp]

theorem int.neg_of_nat_ne_zero (n : ℕ) :

@[simp]

theorem int.zero_ne_neg_of_nat (n : ℕ) :

succ and pred #

def int.succ (a : ℤ) :

Immediate successor of an integer: succ n = n + 1

Equations

a.succ = a + 1

def int.pred (a : ℤ) :

Immediate predecessor of an integer: pred n = n - 1

Equations

a.pred = a - 1

theorem int.nat_succ_eq_int_succ (n : ℕ) :

↑(n.succ) = ↑n.succ

theorem int.pred_succ (a : ℤ) :

a.succ.pred = a

theorem int.succ_pred (a : ℤ) :

a.pred.succ = a

theorem int.neg_succ (a : ℤ) :

-a.succ = (-a).pred

theorem int.succ_neg_succ (a : ℤ) :

(-a.succ).succ = -a

theorem int.neg_pred (a : ℤ) :

-a.pred = (-a).succ

theorem int.pred_neg_pred (a : ℤ) :

(-a.pred).pred = -a

theorem int.pred_nat_succ (n : ℕ) :

↑(n.succ).pred = ↑n

theorem int.neg_nat_succ (n : ℕ) :

-↑(n.succ) = (-↑n).pred

theorem int.succ_neg_nat_succ (n : ℕ) :

(-↑(n.succ)).succ = -↑n

theorem int.add_one_le_iff {a b : ℤ} :

a + 1 ≤ b ↔ a < b

@[norm_cast]

theorem int.coe_pred_of_pos {n : ℕ} (h : 0 < n) :

↑(n - 1) = ↑n - 1

@[protected]

theorem int.induction_on {p : ℤ → Prop} (i : ℤ) (hz : p 0) (hp : ∀ (i : ℕ), p ↑i → p (↑i + 1)) (hn : ∀ (i : ℕ), p (-↑i) → p (-↑i - 1)) :

p i

nat abs #

theorem int.nat_abs_add_le (a b : ℤ) :

(a + b).nat_abs ≤ a.nat_abs + b.nat_abs

theorem int.nat_abs_sub_le (a b : ℤ) :

(a - b).nat_abs ≤ a.nat_abs + b.nat_abs

theorem int.nat_abs_neg_of_nat (n : ℕ) :

(int.neg_of_nat n).nat_abs = n

theorem int.nat_abs_mul (a b : ℤ) :

(a * b).nat_abs = a.nat_abs * b.nat_abs

theorem int.nat_abs_mul_nat_abs_eq {a b : ℤ} {c : ℕ} (h : a * b = ↑c) :

a.nat_abs * b.nat_abs = c

@[simp]

theorem int.nat_abs_mul_self' (a : ℤ) :

↑(a.nat_abs) * ↑(a.nat_abs) = a * a

theorem int.neg_succ_of_nat_eq' (m : ℕ) :

-[1+ m] = -↑m - 1

theorem int.nat_abs_ne_zero_of_ne_zero {z : ℤ} (hz : z ≠ 0) :

z.nat_abs ≠ 0

@[simp]

theorem int.nat_abs_eq_zero {a : ℤ} :

a.nat_abs = 0 ↔ a = 0

theorem int.nat_abs_ne_zero {a : ℤ} :

a.nat_abs ≠ 0 ↔ a ≠ 0

theorem int.nat_abs_lt_nat_abs_of_nonneg_of_lt {a b : ℤ} (w₁ : 0 ≤ a) (w₂ : a < b) :

a.nat_abs < b.nat_abs

theorem int.nat_abs_eq_nat_abs_iff {a b : ℤ} :

a.nat_abs = b.nat_abs ↔ a = b ∨ a = -b

theorem int.nat_abs_eq_iff {a : ℤ} {n : ℕ} :

a.nat_abs = n ↔ a = ↑n ∨ a = -↑n

`/` #

@[simp]

theorem int.of_nat_div (m n : ℕ) :

int.of_nat (m / n) = int.of_nat m / int.of_nat n

@[simp, norm_cast]

theorem int.coe_nat_div (m n : ℕ) :

↑(m / n) = ↑m / ↑n

theorem int.neg_succ_of_nat_div (m : ℕ) {b : ℤ} (H : 0 < b) :

-[1+ m] / b = -(↑m / b + 1)

@[protected]

theorem int.zero_div (b : ℤ) :

0 / b = 0

@[protected]

theorem int.div_zero (a : ℤ) :

a / 0 = 0

@[protected, simp]

theorem int.div_neg (a b : ℤ) :

a / -b = -(a / b)

theorem int.div_of_neg_of_pos {a b : ℤ} (Ha : a < 0) (Hb : 0 < b) :

a / b = -((-a - 1) / b + 1)

@[protected]

theorem int.div_nonneg {a b : ℤ} (Ha : 0 ≤ a) (Hb : 0 ≤ b) :

0 ≤ a / b

theorem int.div_neg' {a b : ℤ} (Ha : a < 0) (Hb : 0 < b) :

a / b < 0

@[protected, simp]

theorem int.div_one (a : ℤ) :

a / 1 = a

theorem int.div_eq_zero_of_lt {a b : ℤ} (H1 : 0 ≤ a) (H2 : a < b) :

a / b = 0

mod #

theorem int.of_nat_mod (m n : ℕ) :

↑m % ↑n = int.of_nat (m % n)

@[simp, norm_cast]

theorem int.coe_nat_mod (m n : ℕ) :

↑(m % n) = ↑m % ↑n

theorem int.neg_succ_of_nat_mod (m : ℕ) {b : ℤ} (bpos : 0 < b) :

-[1+ m] % b = b - 1 - ↑m % b

@[simp]

theorem int.mod_neg (a b : ℤ) :

a % -b = a % b

theorem int.zero_mod (b : ℤ) :

0 % b = 0

theorem int.mod_zero (a : ℤ) :

a % 0 = a

theorem int.mod_one (a : ℤ) :

a % 1 = 0

theorem int.mod_eq_of_lt {a b : ℤ} (H1 : 0 ≤ a) (H2 : a < b) :

a % b = a

theorem int.mod_add_div_aux (m n : ℕ) :

↑n - (↑m % ↑n + 1) - (↑n * (↑m / ↑n) + ↑n) = -[1+ m]

theorem int.mod_add_div (a b : ℤ) :

a % b + b * (a / b) = a

theorem int.div_add_mod (a b : ℤ) :

b * (a / b) + a % b = a

theorem int.mod_add_div' (m k : ℤ) :

m % k + m / k * k = m

theorem int.div_add_mod' (m k : ℤ) :

m / k * k + m % k = m

theorem int.mod_def (a b : ℤ) :

a % b = a - b * (a / b)

properties of `/` and `%` #

@[simp]

theorem int.mul_div_mul_of_pos {a : ℤ} (b c : ℤ) (H : 0 < a) :

a * b / (a * c) = b / c

@[simp]

theorem int.mul_div_mul_of_pos_left (a : ℤ) {b : ℤ} (H : 0 < b) (c : ℤ) :

a * b / (c * b) = a / c

@[simp]

theorem int.mul_mod_mul_of_pos {a : ℤ} (H : 0 < a) (b c : ℤ) :

a * b % (a * c) = a * (b % c)

theorem int.mul_div_cancel_of_mod_eq_zero {a b : ℤ} (H : a % b = 0) :

b * (a / b) = a

theorem int.div_mul_cancel_of_mod_eq_zero {a b : ℤ} (H : a % b = 0) :

a / b * b = a

theorem int.nat_abs_sign (z : ℤ) :

z.sign.nat_abs = ite (z = 0) 0 1

theorem int.nat_abs_sign_of_nonzero {z : ℤ} (hz : z ≠ 0) :

z.sign.nat_abs = 1

theorem int.sign_coe_nat_of_nonzero {n : ℕ} (hn : n ≠ 0) :

@[simp]

theorem int.sign_neg (z : ℤ) :

(-z).sign = -z.sign

theorem int.div_sign (a b : ℤ) :

a / b.sign = a * b.sign

@[simp]

theorem int.sign_mul (a b : ℤ) :

(a * b).sign = a.sign * b.sign

theorem int.mul_sign (i : ℤ) :

i * i.sign = ↑(i.nat_abs)

theorem int.of_nat_add_neg_succ_of_nat_of_lt {m n : ℕ} (h : m < n.succ) :

int.of_nat m + -[1+ n] = -[1+ n - m]

@[simp]

theorem int.neg_add_neg (m n : ℕ) :

-[1+ m] + -[1+ n] = -[1+ (m + n).succ]

to_nat #

theorem int.to_nat_eq_max (a : ℤ) :

↑(a.to_nat) = linear_order.max a 0

@[simp]

theorem int.to_nat_zero :

@[simp]

theorem int.to_nat_one :

@[simp]

theorem int.to_nat_of_nonneg {a : ℤ} (h : 0 ≤ a) :

↑(a.to_nat) = a

@[simp]

theorem int.to_nat_coe_nat (n : ℕ) :

↑n.to_nat = n

@[simp]

theorem int.to_nat_coe_nat_add_one {n : ℕ} :

(↑n + 1).to_nat = n + 1

theorem int.le_to_nat (a : ℤ) :

a ≤ ↑(a.to_nat)

@[simp]

theorem int.le_to_nat_iff {n : ℕ} {z : ℤ} (h : 0 ≤ z) :

n ≤ z.to_nat ↔ ↑n ≤ z

theorem int.to_nat_add {a b : ℤ} (ha : 0 ≤ a) (hb : 0 ≤ b) :

(a + b).to_nat = a.to_nat + b.to_nat

theorem int.to_nat_add_nat {a : ℤ} (ha : 0 ≤ a) (n : ℕ) :

(a + ↑n).to_nat = a.to_nat + n

@[simp]

theorem int.pred_to_nat (i : ℤ) :

(i - 1).to_nat = i.to_nat - 1

@[simp]

theorem int.to_nat_sub_to_nat_neg (n : ℤ) :

↑(n.to_nat) - ↑((-n).to_nat) = n

@[simp]

theorem int.to_nat_add_to_nat_neg_eq_nat_abs (n : ℤ) :

n.to_nat + (-n).to_nat = n.nat_abs

def int.to_nat' :

ℤ → option ℕ

If n : ℕ, then int.to_nat' n = some n, if n : ℤ is negative, then int.to_nat' n = none.

Equations

-[1+ n].to_nat' = option.none
↑n.to_nat' = option.some n

theorem int.mem_to_nat' (a : ℤ) (n : ℕ) :

n ∈ a.to_nat' ↔ a = ↑n

@[simp]

theorem int.to_nat_neg_nat (n : ℕ) :

(-↑n).to_nat = 0