Documentation

Mathlib.Data.Nat.Order.Lemmas

Further lemmas about the natural numbers #

The distinction between this file and Mathlib.Data.Nat.Order.Basic is not particularly clear. They are separated for now to minimize the porting requirements for tactics during the transition to mathlib4. After Mathlib.Data.Rat.Order has been ported, please feel free to reorganize these two files.

Sets #

instance Nat.Subtype.orderBot (s : Set ) [DecidablePred fun (x : ) => x s] [h : Nonempty s] :
Equations
Equations
  • One or more equations did not get rendered due to their size.
theorem Nat.Subtype.coe_bot {s : Set } [DecidablePred fun (x : ) => x s] [h : Nonempty s] :
= Nat.find (_ : ∃ (a : ), a s)
theorem Nat.set_eq_univ {S : Set } :
S = Set.univ 0 S kS, k + 1 S

div #

theorem Nat.lt_div_iff_mul_lt {n : } {d : } (hnd : d n) (a : ) :
a < n / d d * a < n
theorem Nat.mul_div_eq_iff_dvd {n : } {d : } :
d * (n / d) = n d n
theorem Nat.mul_div_lt_iff_not_dvd {n : } {d : } :
d * (n / d) < n ¬d n
theorem Nat.div_eq_iff_eq_of_dvd_dvd {n : } {x : } {y : } (hn : n 0) (hx : x n) (hy : y n) :
n / x = n / y x = y
theorem Nat.div_eq_zero_iff {a : } {b : } (hb : 0 < b) :
a / b = 0 a < b
theorem Nat.div_ne_zero_iff {a : } {b : } (hb : b 0) :
a / b 0 b a
theorem Nat.div_pos_iff {a : } {b : } (hb : b 0) :
0 < a / b b a

mod, dvd #

@[simp]
theorem Nat.not_two_dvd_bit1 (n : ) :
@[simp]
theorem Nat.dvd_add_self_left {m : } {n : } :
m m + n m n

A natural number m divides the sum m + n if and only if m divides n.

@[simp]
theorem Nat.dvd_add_self_right {m : } {n : } :
m n + m m n

A natural number m divides the sum n + m if and only if m divides n.

theorem Nat.dvd_sub' {k : } {m : } {n : } (h₁ : k m) (h₂ : k n) :
k m - n
theorem Nat.succ_div (a : ) (b : ) :
(a + 1) / b = a / b + if b a + 1 then 1 else 0
theorem Nat.succ_div_of_dvd {a : } {b : } (hba : b a + 1) :
(a + 1) / b = a / b + 1
theorem Nat.succ_div_of_not_dvd {a : } {b : } (hba : ¬b a + 1) :
(a + 1) / b = a / b
theorem Nat.dvd_iff_div_mul_eq (n : ) (d : ) :
d n n / d * d = n
theorem Nat.dvd_iff_le_div_mul (n : ) (d : ) :
d n n n / d * d
theorem Nat.dvd_iff_dvd_dvd (n : ) (d : ) :
d n ∀ (k : ), k dk n
theorem Nat.dvd_div_of_mul_dvd {a : } {b : } {c : } (h : a * b c) :
b c / a
@[simp]
theorem Nat.dvd_div_iff {a : } {b : } {c : } (hbc : c b) :
a b / c c * a b
@[simp]
theorem Nat.div_div_div_eq_div {a : } {b : } {c : } (dvd : b a) (dvd2 : a c) :
c / (a / b) / b = c / a
theorem Nat.eq_zero_of_dvd_of_lt {a : } {b : } (w : a b) (h : b < a) :
b = 0

If a small natural number is divisible by a larger natural number, the small number is zero.

theorem Nat.le_of_lt_add_of_dvd {a : } {b : } {n : } (h : a < b + n) :
n an ba b
theorem Nat.not_dvd_iff_between_consec_multiples (n : ) {a : } (ha : 0 < a) :
(∃ (k : ), a * k < n n < a * (k + 1)) ¬a n

n is not divisible by a iff it is between a * k and a * (k + 1) for some k.

theorem Nat.dvd_right_iff_eq {m : } {n : } :
(∀ (a : ), m a n a) m = n

Two natural numbers are equal if and only if they have the same multiples.

theorem Nat.dvd_left_iff_eq {m : } {n : } :
(∀ (a : ), a m a n) m = n

Two natural numbers are equal if and only if they have the same divisors.

theorem Nat.dvd_left_injective :
Function.Injective fun (x x_1 : ) => x x_1

dvd is injective in the left argument

theorem Nat.div_lt_div_of_lt_of_dvd {a : } {b : } {d : } (hdb : d b) (h : a < b) :
a / d < b / d