Documentation

Mathlib.Data.Int.Defs

Basic operations on the integers #

This file contains some basic lemmas about integers.

See note [foundational algebra order theory].

TODO #

Split this file into:

theorem Int.le_rfl {a : } :
a a
theorem Int.lt_or_lt_of_ne {a : } {b : } :
a ba < b b < a
theorem Int.lt_or_le (a : ) (b : ) :
a < b b a
theorem Int.le_or_lt (a : ) (b : ) :
a b b < a
theorem Int.lt_asymm {a : } {b : } :
a < b¬b < a
theorem Int.le_of_eq {a : } {b : } (hab : a = b) :
a b
theorem Int.ge_of_eq {a : } {b : } (hab : a = b) :
b a
theorem Int.le_antisymm_iff {a : } {b : } :
a = b a b b a
theorem Int.le_iff_eq_or_lt {a : } {b : } :
a b a = b a < b
theorem Int.le_iff_lt_or_eq {a : } {b : } :
a b a < b a = b
theorem Int.one_pos :
0 < 1
theorem Int.neg_eq_neg {a : } {b : } (h : -a = -b) :
a = b
@[simp]
theorem Int.neg_pos {a : } :
0 < -a a < 0
@[simp]
theorem Int.neg_nonneg {a : } :
0 -a a 0
@[simp]
theorem Int.neg_neg_iff_pos {a : } :
-a < 0 0 < a
@[simp]
theorem Int.neg_nonpos_iff_nonneg {a : } :
-a 0 0 a
@[simp]
theorem Int.sub_pos {a : } {b : } :
0 < a - b b < a
@[simp]
theorem Int.sub_nonneg {a : } {b : } :
0 a - b b a
theorem Int.ofNat_add_out (m : ) (n : ) :
m + n = (m + n)
theorem Int.ofNat_mul_out (m : ) (n : ) :
m * n = (m * n)
theorem Int.ofNat_add_one_out (n : ) :
n + 1 = n.succ
@[simp]
theorem Int.ofNat_eq_natCast (n : ) :
Int.ofNat n = n
@[deprecated Int.ofNat_eq_natCast]
theorem Int.natCast_eq_ofNat (n : ) :
n = Int.ofNat n
theorem Int.natCast_inj {m : } {n : } :
m = n m = n
@[simp]
theorem Int.natAbs_cast (n : ) :
(↑n).natAbs = n
theorem Int.natCast_sub {n : } {m : } :
n m(m - n) = m - n
@[simp]
theorem Int.natCast_eq_zero {n : } :
n = 0 n = 0
theorem Int.natCast_ne_zero {n : } :
n 0 n 0
theorem Int.natCast_ne_zero_iff_pos {n : } :
n 0 0 < n
@[simp]
theorem Int.natCast_pos {n : } :
0 < n 0 < n
theorem Int.natCast_succ_pos (n : ) :
0 < n.succ
@[simp]
theorem Int.natCast_nonpos_iff {n : } :
n 0 n = 0
theorem Int.natCast_nonneg (n : ) :
0 n
@[simp]
theorem Int.sign_natCast_add_one (n : ) :
(n + 1).sign = 1
@[simp]
theorem Int.cast_id {n : } :
n = n
theorem Int.two_mul (n : ) :
2 * n = n + n
theorem Int.mul_le_mul_iff_of_pos_right {a : } {b : } {c : } (ha : 0 < a) :
b * a c * a b c
theorem Int.mul_nonneg_iff_of_pos_right {a : } {b : } (hb : 0 < b) :
0 a * b 0 a

succ and pred #

def Int.succ (a : ) :

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

Equations
  • a.succ = a + 1
Instances For
    def Int.pred (a : ) :

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

    Equations
    • a.pred = a - 1
    Instances For
      theorem Int.natCast_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_natCast_succ (n : ) :
      (-n.succ).succ = -n
      theorem Int.natCast_pred_of_pos {n : } (h : 0 < n) :
      (n - 1) = n - 1
      theorem Int.lt_succ_self (a : ) :
      a < a.succ
      theorem Int.pred_self_lt (a : ) :
      a.pred < a
      theorem Int.le_add_one_iff {m : } {n : } :
      m n + 1 m n m = n + 1
      theorem Int.sub_one_lt_iff {m : } {n : } :
      m - 1 < n m n
      theorem Int.le_sub_one_iff {m : } {n : } :
      m n - 1 m < n

      The following few lemmas are proved in the core implementation of the omega tactic. We expose them here with nice user-facing names.

      theorem Int.add_le_iff_le_sub {a : } {b : } {c : } :
      a + b c a c - b
      theorem Int.le_add_iff_sub_le {a : } {b : } {c : } :
      a b + c a - c b
      theorem Int.add_le_zero_iff_le_neg {a : } {b : } :
      a + b 0 a -b
      theorem Int.add_le_zero_iff_le_neg' {a : } {b : } :
      a + b 0 b -a
      theorem Int.add_nonnneg_iff_neg_le {a : } {b : } :
      0 a + b -b a
      theorem Int.add_nonnneg_iff_neg_le' {a : } {b : } :
      0 a + b -a b
      theorem Int.induction_on {p : Prop} (i : ) (hz : p 0) (hp : ∀ (i : ), p ip (i + 1)) (hn : ∀ (i : ), p (-i)p (-i - 1)) :
      p i
      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.inductionOn'_self {C : Sort u_1} {b : } {H0 : C b} {Hs : (k : ) → b kC kC (k + 1)} {Hp : (k : ) → k bC kC (k - 1)} :
            b.inductionOn' b H0 Hs Hp = H0
            theorem Int.inductionOn'_add_one {C : Sort u_1} {z : } {b : } {H0 : C b} {Hs : (k : ) → b kC kC (k + 1)} {Hp : (k : ) → k bC kC (k - 1)} (hz : b z) :
            (z + 1).inductionOn' b H0 Hs Hp = Hs z hz (z.inductionOn' b H0 Hs Hp)
            theorem Int.inductionOn'_sub_one {C : Sort u_1} {z : } {b : } {H0 : C b} {Hs : (k : ) → b kC kC (k + 1)} {Hp : (k : ) → k bC kC (k - 1)} (hz : z b) :
            (z - 1).inductionOn' b H0 Hs Hp = Hp z hz (z.inductionOn' b H0 Hs Hp)
            def Int.negInduction {C : Sort u_1} (nat : (n : ) → C n) (neg : (n : ) → C nC (-n)) (n : ) :
            C n

            Inductively define a function on by defining it on and extending it from n to -n.

            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.

              def Int.strongRec {m : } {P : Sort u_1} (lt : (n : ) → n < mP n) (ge : (n : ) → n m((k : ) → k < nP k)P n) (n : ) :
              P n

              A strong recursor for Int that specifies explicit values for integers below a threshold, and is analogous to Nat.strongRec for integers on or above the threshold.

              Equations
              • One or more equations did not get rendered due to their size.
              Instances For
                theorem Int.strongRec_of_lt {m : } {n : } {P : Sort u_1} {lt : (n : ) → n < mP n} {ge : (n : ) → n m((k : ) → k < nP k)P n} (hn : n < m) :
                Int.strongRec lt ge n = lt n hn
                theorem Int.strongRec_of_ge {m : } {n : } {P : Sort u_1} {lt : (n : ) → n < mP n} {ge : (n : ) → n m((k : ) → k < nP k)P n} (hn : m n) :
                Int.strongRec lt ge n = ge n hn fun (k : ) (x : k < n) => Int.strongRec lt ge k

                nat abs #

                @[simp]
                theorem Int.natAbs_ofNat' (n : ) :
                (Int.ofNat n).natAbs = n
                theorem Int.natAbs_add_of_nonneg {a : } {b : } :
                0 a0 b(a + b).natAbs = a.natAbs + b.natAbs
                theorem Int.natAbs_add_of_nonpos {a : } {b : } (ha : a 0) (hb : b 0) :
                (a + b).natAbs = a.natAbs + b.natAbs
                theorem Int.natAbs_pow (n : ) (k : ) :
                (n ^ k).natAbs = n.natAbs ^ k
                theorem Int.pow_right_injective {a : } (h : 1 < a.natAbs) :
                Function.Injective fun (x : ) => a ^ x
                theorem Int.natAbs_sq (x : ) :
                x.natAbs ^ 2 = x ^ 2
                theorem Int.natAbs_pow_two (x : ) :
                x.natAbs ^ 2 = x ^ 2

                Alias of Int.natAbs_sq.

                / #

                @[simp]
                theorem Int.natCast_div (m : ) (n : ) :
                (m / n) = m / n
                theorem Int.natCast_ediv (m : ) (n : ) :
                (m / n) = (↑m).ediv n
                theorem Int.ediv_of_neg_of_pos {a : } {b : } (Ha : a < 0) (Hb : 0 < b) :
                a.ediv b = -((-a - 1) / b + 1)

                mod #

                @[simp]
                theorem Int.natCast_mod (m : ) (n : ) :
                (m % n) = m % n
                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.emod_two_eq_zero_or_one (n : ) :
                n % 2 = 0 n % 2 = 1

                dvd #

                theorem Int.mul_dvd_mul {a : } {b : } {c : } {d : } :
                a bc da * c b * d
                theorem Int.mul_dvd_mul_left {b : } {c : } (a : ) (h : b c) :
                a * b a * c
                theorem Int.mul_dvd_mul_right {b : } {c : } (a : ) (h : b c) :
                b * a c * a
                theorem Int.dvd_mul_of_div_dvd {a : } {b : } {c : } (h : b a) (hdiv : a / b c) :
                a b * c
                @[simp]
                theorem Int.div_dvd_iff_dvd_mul {a : } {b : } {c : } (h : b a) (hb : b 0) :
                a / b c a b * c
                theorem Int.mul_dvd_of_dvd_div {a : } {b : } {c : } (hcb : c b) (h : a b / c) :
                c * a b
                theorem Int.dvd_div_of_mul_dvd {a : } {b : } {c : } (h : a * b c) :
                b c / a
                @[simp]
                theorem Int.dvd_div_iff_mul_dvd {a : } {b : } {c : } (hbc : c b) :
                a b / c c * a b
                theorem Int.ediv_dvd_ediv {a : } {b : } {c : } :
                a bb cb / a c / a
                theorem Int.exists_lt_and_lt_iff_not_dvd {n : } (m : ) (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.natCast_dvd_natCast {m : } {n : } :
                m n m n
                theorem Int.natCast_dvd {n : } {m : } :
                m n m n.natAbs
                theorem Int.dvd_natCast {m : } {n : } :
                m n m.natAbs n
                theorem Int.natAbs_ediv (a : ) (b : ) (H : b a) :
                (a / b).natAbs = a.natAbs / b.natAbs
                theorem Int.dvd_of_mul_dvd_mul_left {a : } {m : } {n : } (ha : a 0) (h : a * m a * n) :
                m n
                theorem Int.dvd_of_mul_dvd_mul_right {a : } {m : } {n : } (ha : a 0) (h : m * a n * a) :
                m n
                theorem Int.eq_mul_div_of_mul_eq_mul_of_dvd_left {a : } {b : } {c : } {d : } (hb : b 0) (hbc : b c) (h : b * a = c * d) :
                a = c / b * d
                theorem Int.eq_zero_of_dvd_of_natAbs_lt_natAbs {m : } {n : } (hmn : m n) (hnm : n.natAbs < m.natAbs) :
                n = 0

                If an integer with larger absolute value divides an integer, it is zero.

                theorem Int.eq_zero_of_dvd_of_nonneg_of_lt {m : } {n : } (hm : 0 m) (hmn : m < n) (hnm : n m) :
                m = 0
                theorem Int.eq_of_mod_eq_of_natAbs_sub_lt_natAbs {a : } {b : } {c : } (h1 : a % b = c) (h2 : (a - c).natAbs < b.natAbs) :
                a = c

                If two integers are congruent to a sufficiently large modulus, they are equal.

                theorem Int.ofNat_add_negSucc_of_ge {m : } {n : } (h : n.succ m) :
                theorem Int.natAbs_le_of_dvd_ne_zero {m : } {n : } (hmn : m n) (hn : n 0) :
                m.natAbs n.natAbs
                @[deprecated Int.natCast_dvd_natCast]
                theorem Int.coe_nat_dvd {m : } {n : } :
                m n m n

                Alias of Int.natCast_dvd_natCast.

                @[deprecated Int.dvd_natCast]
                theorem Int.coe_nat_dvd_right {m : } {n : } :
                m n m.natAbs n

                Alias of Int.dvd_natCast.

                @[deprecated Int.natCast_dvd]
                theorem Int.coe_nat_dvd_left {n : } {m : } :
                m n m n.natAbs

                Alias of Int.natCast_dvd.

                / and ordering #

                theorem Int.natAbs_eq_of_dvd_dvd {m : } {n : } (hmn : m n) (hnm : n m) :
                m.natAbs = n.natAbs
                theorem Int.ediv_dvd_of_dvd {m : } {n : } (hmn : m n) :
                n / m n
                theorem Int.le_iff_pos_of_dvd {a : } {b : } (ha : 0 < a) (hab : a b) :
                a b 0 < b
                theorem Int.le_add_iff_lt_of_dvd_sub {a : } {b : } {c : } (ha : 0 < a) (hab : a c - b) :
                a + b c b < c

                sign #

                theorem Int.sign_natCast_of_ne_zero {n : } (hn : n 0) :
                (↑n).sign = 1
                theorem Int.sign_add_eq_of_sign_eq {m : } {n : } :
                m.sign = n.sign(m + n).sign = n.sign

                toNat #

                @[simp]
                theorem Int.toNat_natCast (n : ) :
                (↑n).toNat = n
                @[simp]
                theorem Int.toNat_natCast_add_one {n : } :
                (n + 1).toNat = n + 1
                @[simp]
                theorem Int.toNat_le {m : } {n : } :
                m.toNat n m n
                @[simp]
                theorem Int.lt_toNat {n : } {m : } :
                m < n.toNat m < n
                theorem Int.toNat_le_toNat {a : } {b : } (h : a b) :
                a.toNat b.toNat
                theorem Int.toNat_lt_toNat {a : } {b : } (hb : 0 < b) :
                a.toNat < b.toNat a < b
                theorem Int.lt_of_toNat_lt {a : } {b : } (h : a.toNat < b.toNat) :
                a < b
                @[simp]
                theorem Int.toNat_pred_coe_of_pos {i : } (h : 0 < i) :
                (i.toNat - 1) = i - 1
                @[simp]
                theorem Int.toNat_eq_zero {n : } :
                n.toNat = 0 n 0
                @[simp]
                theorem Int.toNat_sub_of_le {a : } {b : } (h : b a) :
                (a - b).toNat = a - b
                @[deprecated Int.natCast_pos]
                theorem Int.coe_nat_pos {n : } :
                0 < n 0 < n

                Alias of Int.natCast_pos.

                @[deprecated Int.natCast_succ_pos]
                theorem Int.coe_nat_succ_pos (n : ) :
                0 < n.succ

                Alias of Int.natCast_succ_pos.

                theorem Int.toNat_lt' {m : } {n : } (hn : n 0) :
                m.toNat < n m < n
                def Int.natMod (m : ) (n : ) :

                The modulus of an integer by another as a natural. Uses the E-rounding convention.

                Equations
                • m.natMod n = (m % n).toNat
                Instances For
                  theorem Int.natMod_lt {m : } {n : } (hn : n 0) :
                  m.natMod n < n
                  @[deprecated Int.natCast_pow]
                  theorem Int.coe_nat_pow (b : ) (n : ) :
                  (b ^ n) = b ^ n

                  Alias of Int.natCast_pow.

                  @[simp]
                  theorem Int.pow_eq (m : ) (n : ) :
                  m.pow n = m ^ n
                  @[deprecated Int.ofNat_eq_natCast]
                  theorem Int.ofNat_eq_cast (n : ) :
                  Int.ofNat n = n

                  Alias of Int.ofNat_eq_natCast.

                  @[deprecated Int.natCast_inj]
                  theorem Int.cast_eq_cast_iff_Nat {m : } {n : } :
                  m = n m = n

                  Alias of Int.natCast_inj.

                  @[deprecated Int.natCast_sub]
                  theorem Int.coe_nat_sub {n : } {m : } :
                  n m(m - n) = m - n

                  Alias of Int.natCast_sub.

                  @[deprecated Int.natCast_nonneg]
                  theorem Int.coe_nat_nonneg (n : ) :
                  0 n

                  Alias of Int.natCast_nonneg.

                  @[deprecated Int.sign_natCast_add_one]
                  theorem Int.sign_coe_add_one (n : ) :
                  (n + 1).sign = 1

                  Alias of Int.sign_natCast_add_one.

                  @[deprecated Int.natCast_succ]
                  theorem Int.nat_succ_eq_int_succ (n : ) :
                  n.succ = (↑n).succ

                  Alias of Int.natCast_succ.

                  @[deprecated Int.succ_neg_natCast_succ]
                  theorem Int.succ_neg_nat_succ (n : ) :
                  (-n.succ).succ = -n

                  Alias of Int.succ_neg_natCast_succ.

                  @[deprecated Int.natCast_pred_of_pos]
                  theorem Int.coe_pred_of_pos {n : } (h : 0 < n) :
                  (n - 1) = n - 1

                  Alias of Int.natCast_pred_of_pos.

                  @[deprecated Int.natCast_div]
                  theorem Int.coe_nat_div (m : ) (n : ) :
                  (m / n) = m / n

                  Alias of Int.natCast_div.

                  @[deprecated Int.natCast_ediv]
                  theorem Int.coe_nat_ediv (m : ) (n : ) :
                  (m / n) = (↑m).ediv n

                  Alias of Int.natCast_ediv.

                  @[deprecated Int.sign_natCast_of_ne_zero]
                  theorem Int.sign_coe_nat_of_nonzero {n : } (hn : n 0) :
                  (↑n).sign = 1

                  Alias of Int.sign_natCast_of_ne_zero.

                  @[deprecated Int.toNat_natCast]
                  theorem Int.toNat_coe_nat (n : ) :
                  (↑n).toNat = n

                  Alias of Int.toNat_natCast.

                  @[deprecated Int.toNat_natCast_add_one]
                  theorem Int.toNat_coe_nat_add_one {n : } :
                  (n + 1).toNat = n + 1

                  Alias of Int.toNat_natCast_add_one.