Documentation

Mathlib.Data.Int.Order.Basic

Order instances on the integers #

This file contains:

Recursors #

Extra instances to short-circuit type class resolution #

Equations
Equations
theorem Int.abs_eq_natAbs (a : ) :
|a| = (Int.natAbs a)
@[simp]
theorem Int.coe_natAbs (n : ) :
(Int.natAbs n) = |n|
theorem Nat.cast_natAbs {α : Type u_1} [AddGroupWithOne α] (n : ) :
(Int.natAbs n) = |n|
theorem Int.sign_mul_abs (a : ) :
Int.sign a * |a| = a
theorem Int.natAbs_sq (x : ) :
(Int.natAbs x) ^ 2 = x ^ 2
theorem Int.natAbs_pow_two (x : ) :
(Int.natAbs x) ^ 2 = x ^ 2

Alias of Int.natAbs_sq.

theorem Int.natAbs_le_self_sq (a : ) :
(Int.natAbs a) a ^ 2
theorem Int.le_self_sq (b : ) :
b b ^ 2
theorem Int.le_self_pow_two (b : ) :
b b ^ 2

Alias of Int.le_self_sq.

theorem Int.coe_nat_eq_zero {n : } :
n = 0 n = 0
theorem Int.coe_nat_ne_zero {n : } :
n 0 n 0
theorem Int.coe_nat_ne_zero_iff_pos {n : } :
n 0 0 < n
theorem Int.abs_coe_nat (n : ) :
|n| = n
theorem Int.cast_mul_eq_zsmul_cast {α : Type u_1} [AddCommGroupWithOne α] (m : ) (n : ) :
(m * n) = m n

Note this holds in marginally more generality than Int.cast_mul

theorem Int.natAbs_sub_pos_iff {i : } {j : } :
0 < Int.natAbs (i - j) i j
theorem Int.natAbs_sub_ne_zero_iff {i : } {j : } :
Int.natAbs (i - j) 0 i j

succ and pred #

theorem Int.le_add_one_iff {m : } {n : } :
m n + 1 m n m = n + 1
theorem Int.sub_one_lt_iff {a : } {b : } :
a - 1 < b a b
theorem Int.le_sub_one_iff {a : } {b : } :
a b - 1 a < b
@[simp]
theorem Int.abs_lt_one_iff {a : } :
|a| < 1 a = 0
theorem Int.abs_le_one_iff {a : } :
|a| 1 a = 0 a = 1 a = -1
theorem Int.one_le_abs {z : } (h₀ : z 0) :
1 |z|
def Int.inductionOn' {C : Sort u_1} (z : ) (b : ) (H0 : C b) (Hs : (k : ) → b kC kC (k + 1)) (Hp : (k : ) → k bC kC (k - 1)) :
C z

Inductively define a function on by defining it at b, for the succ of a number greater than b, and the pred of a number less than b.

Equations
Instances For
    def Int.inductionOn'.pos {C : Sort u_1} (b : ) (H0 : C b) (Hs : (k : ) → b kC kC (k + 1)) (n : ) :
    C (b + n)

    The positive case of Int.inductionOn'.

    Equations
    Instances For
      def Int.inductionOn'.neg {C : Sort u_1} (b : ) (H0 : C b) (Hp : (k : ) → k bC kC (k - 1)) (n : ) :
      C (b + Int.negSucc n)

      The negative case of Int.inductionOn'.

      Equations
      Instances For
        theorem Int.le_induction {P : Prop} {m : } (h0 : P m) (h1 : ∀ (n : ), m nP nP (n + 1)) (n : ) :
        m nP n

        See Int.inductionOn' for an induction in both directions.

        theorem Int.le_induction_down {P : Prop} {m : } (h0 : P m) (h1 : ∀ (n : ), n mP nP (n - 1)) (n : ) :
        n mP n

        See Int.inductionOn' for an induction in both directions.

        nat abs #

        / #

        theorem Int.ediv_eq_zero_of_lt_abs {a : } {b : } (H1 : 0 a) (H2 : a < |b|) :
        a / b = 0

        mod #

        @[simp]
        theorem Int.emod_abs (a : ) (b : ) :
        a % |b| = a % b
        theorem Int.emod_lt (a : ) {b : } (H : b 0) :
        a % b < |b|
        theorem Int.add_emod_eq_add_mod_right {m : } {n : } {k : } (i : ) (H : m % n = k % n) :
        (m + i) % n = (k + i) % n
        @[simp]
        theorem Int.neg_emod_two (i : ) :
        -i % 2 = i % 2

        properties of / and % #

        theorem Int.abs_ediv_le_abs (a : ) (b : ) :
        |a / b| |a|
        theorem Int.emod_two_eq_zero_or_one (n : ) :
        n % 2 = 0 n % 2 = 1

        dvd #

        theorem Int.ediv_dvd_ediv {a : } {b : } {c : } :
        a bb cb / a c / a
        theorem Int.abs_sign_of_nonzero {z : } (hz : z 0) :
        |Int.sign z| = 1
        theorem Int.exists_lt_and_lt_iff_not_dvd (m : ) {n : } (hn : 0 < n) :
        (∃ (k : ), n * k < m m < n * (k + 1)) ¬n m

        If n > 0 then m is not divisible by n iff it is between n * k and n * (k + 1) for some k.

        theorem Int.sign_eq_ediv_abs (a : ) :
        Int.sign a = a / |a|

        / and ordering #

        theorem Int.natAbs_eq_of_dvd_dvd {s : } {t : } (hst : s t) (hts : t s) :
        theorem Int.ediv_dvd_of_dvd {s : } {t : } (hst : s t) :
        t / s t

        toNat #

        @[simp]
        theorem Int.toNat_le {a : } {n : } :
        Int.toNat a n a n
        @[simp]
        theorem Int.lt_toNat {n : } {a : } :
        n < Int.toNat a n < a
        @[simp]
        theorem Int.coe_nat_nonpos_iff {n : } :
        n 0 n = 0
        theorem Int.toNat_le_toNat {a : } {b : } (h : a b) :
        theorem Int.toNat_lt_toNat {a : } {b : } (hb : 0 < b) :
        theorem Int.lt_of_toNat_lt {a : } {b : } (h : Int.toNat a < Int.toNat b) :
        a < b
        @[simp]
        theorem Int.toNat_pred_coe_of_pos {i : } (h : 0 < i) :
        (Int.toNat i - 1) = i - 1
        @[simp]
        theorem Int.toNat_eq_zero {n : } :
        Int.toNat n = 0 n 0
        @[simp]
        theorem Int.toNat_sub_of_le {a : } {b : } (h : b a) :
        (Int.toNat (a - b)) = a - b
        @[simp]
        theorem abs_zsmul_eq_zero {G : Type u_1} [AddGroup G] (a : G) (n : ) :
        |n| a = 0 n a = 0
        @[simp]
        theorem zpow_abs_eq_one {G : Type u_1} [Group G] (a : G) (n : ) :
        a ^ |n| = 1 a ^ n = 1
        theorem bit0_mul {R : Type u_1} [NonUnitalNonAssocRing R] (n : R) (r : R) :
        bit0 n * r = 2 (n * r)
        theorem mul_bit0 {R : Type u_1} [NonUnitalNonAssocRing R] (n : R) (r : R) :
        r * bit0 n = 2 (r * n)
        theorem bit1_mul {R : Type u_1} [NonAssocRing R] (n : R) (r : R) :
        bit1 n * r = 2 (n * r) + r
        theorem mul_bit1 {R : Type u_1} [NonAssocRing R] {n : R} {r : R} :
        r * bit1 n = 2 (r * n) + r