ℤ facts

def Int.rdiv (a : ℤ) (b : ℕ) (up : Bool) : ℤ

Int division, rounding up or down

Equations

• a.rdiv b up = bif up then -(-a / ↑b) else a / ↑b

theorem Int.rdiv_nonneg {a : ℤ} {b : ℕ} {up : Bool} (a0 : 0 ≤ a) : 0 ≤ a.rdiv b up

0 ≤ rdiv a _ _ if 0 ≤ a

theorem Int.rdiv_le {a : ℤ} {b : ℕ} : ↑(a.rdiv b false) ≤ ↑a / ↑b

rdiv rounds down if desired

theorem Int.le_rdiv {a : ℤ} {b : ℕ} : ↑a / ↑b ≤ ↑(a.rdiv b true)

rdiv rounds up if desired

theorem Int.rdiv_le_rdiv {a : ℤ} {b : ℕ} {u0 u1 : Bool} (u01 : u0 ≤ u1) : a.rdiv b u0 ≤ a.rdiv b u1

@[simp]

theorem Int.zero_rdiv {b : ℕ} {up : Bool} : rdiv 0 b up = 0

@[simp]

theorem Int.rdiv_one {a : ℤ} {up : Bool} : a.rdiv 1 up = a

rdiv by 1 does nothing

theorem Int.rdiv_lt {a : ℤ} {b : ℕ} {up : Bool} : ↑(a.rdiv b up) < ↑a / ↑b + 1

rdiv never rounds up by much

theorem Int.abs_rdiv_le (x : ℤ) (y : ℕ) (up : Bool) : |x.rdiv y up| ≤ |x|

rdiv reduces abs

theorem Int.rdiv_div {a : ℤ} {b c : ℕ} (bc : c ∣ b) : a.rdiv (b / c) = (a * ↑c).rdiv b

a.rdiv (b / c) = (a * c).rdiv b if c | b

@[simp]

theorem Int.mul_rdiv_cancel {a : ℤ} {b : ℕ} (b0 : b ≠ 0) {up : Bool} : (a * ↑b).rdiv b up = a

theorem Int.ediv_eq_neg_one {a b : ℤ} (a0 : 0 < a) (ab : a ≤ b) : -a / b = -1

Int.ediv (-small) big = -1

theorem Int.ediv_eq_neg_one' {a b : ℤ} (a0 : a < 0) (b0 : 0 < b) (ab : -a < b) : a / b = -1

A sufficient condition for Int.ediv = -1

theorem Int.neg_ediv_neg {a b : ℤ} (b0 : 0 < b) (ab : ¬b ∣ a) : -(-a / b) = a / b + 1

-(-a / b) rounds up if we don't divide

theorem Int.ediv_pow_of_le {a : ℤ} {n k : ℕ} (a0 : a ≠ 0) (kn : k ≤ n) : a ^ n / a ^ k = a ^ (n - k)

a ^ n / a ^ k = a ^ (n - k) if k ≤ n

theorem Int.neg_ediv_pow_of_le {a : ℤ} {n k : ℕ} (a0 : a ≠ 0) (kn : k ≤ n) : -a ^ n / a ^ k = -a ^ (n - k)

-a ^ n / a ^ k = -a ^ (n - k) if k ≤ n

theorem Int.cast_neg_ceilDiv_eq_ediv (a b : ℕ) : -↑(a ⌈/⌉ b) = -↑a / ↑b

ℕ's -ceilDiv in terms of Int.ediv

theorem Int.cast_ceilDiv_eq_neg_ediv (a b : ℕ) : ↑(a ⌈/⌉ b) = -(-↑a / ↑b)

ℕ's ceilDiv in terms of Int.ediv

theorem Int.natAbs_eq_toNat {a : ℤ} (a0 : 0 ≤ a) : a.natAbs = a.toNat

natAbs = toNat if we're nonnegative

theorem Int.natAbs_eq_toNat_neg {a : ℤ} (a0 : a ≤ 0) : a.natAbs = (-a).toNat

natAbs = toNat - if we're nonpositive

theorem Int.coe_natAbs_eq_self {R : Type u_1} [Ring R] [LinearOrder R] [IsStrictOrderedRing R] {a : ℤ} (h : 0 ≤ a) : ↑a.natAbs = ↑a

Coercion of natAbs to any linearly ordered ring is equal to a for nonnegative a

theorem Int.coe_natAbs_eq_neg {R : Type u_1} [Ring R] [LinearOrder R] [IsStrictOrderedRing R] {a : ℤ} (h : a ≤ 0) : ↑a.natAbs = -↑a

Coercion of natAbs to any linearly ordered ring is equal to -a for nonpositive a

theorem Int.emod_mul_eq_mul_emod' (a n m : ℤ) (n0 : 0 ≤ n) (m0 : 0 < m) : a * n % (m * n) = a % m * n

theorem Int.emod_mul_eq_mul_emod (a n : ℤ) (n0 : 0 < n) : a * n % n ^ 2 = a % n * n

theorem Int.induction_overlap {p : ℤ → Prop} (hi : ∀ (n : ℕ), p ↑n) (lo : ∀ (n : ℕ), p (-↑n)) (n : ℤ) : p n

p is true for all integers if it is true for nonnegative and nonpositive integers.

This is a slightly nicer induction principle on the integers that covers zero twice to reduce notational clutter.

theorem zpow_anti {𝕜 : Type u_1} [Semifield 𝕜] [LinearOrder 𝕜] [IsStrictOrderedRing 𝕜] {a : 𝕜} (a0 : 0 < a) (a1 : a ≤ 1) : Antitone fun (n : ℤ) => a ^ n

theorem Bound.zpow_le_zpow_right_of_le_one_or_one_le {𝕜 : Type u_1} [Semifield 𝕜] [LinearOrder 𝕜] [IsStrictOrderedRing 𝕜] {a : 𝕜} {n m : ℤ} (h : 1 ≤ a ∧ n ≤ m ∨ 0 < a ∧ a ≤ 1 ∧ m ≤ n) : a ^ n ≤ a ^ m

bound lemma for branching on 1 ≤ a ∨ a ≤ 1 when proving a ^ n ≤ a ^ m

@[simp]

theorem Int.natFloor_cast (n : ℤ) : ⌊↑n⌋₊ = ⌊n⌋₊

theorem Int.abs_def {n : ℤ} : |n| = if n < 0 then -n else n

Turn |n| into something omega understands

theorem Int.natAbs_def {n : ℤ} : n.natAbs = if n < 0 then (-n).toNat else n.toNat

Turn n.natAbs into something omega understands