mathlib docs: data.nat.basic

nat.canonically_ordered_comm_semiring = {add := ordered_add_comm_monoid.add infer_instance, add_assoc := nat.canonically_ordered_comm_semiring._proof_1, zero := ordered_add_comm_monoid.zero infer_instance, zero_add := nat.canonically_ordered_comm_semiring._proof_2, add_zero := nat.canonically_ordered_comm_semiring._proof_3, add_comm := nat.canonically_ordered_comm_semiring._proof_4, le := ordered_add_comm_monoid.le infer_instance, lt := ordered_add_comm_monoid.lt infer_instance, le_refl := nat.canonically_ordered_comm_semiring._proof_5, le_trans := nat.canonically_ordered_comm_semiring._proof_6, lt_iff_le_not_le := nat.canonically_ordered_comm_semiring._proof_7, le_antisymm := nat.canonically_ordered_comm_semiring._proof_8, add_le_add_left := nat.canonically_ordered_comm_semiring._proof_9, lt_of_add_lt_add_left := nat.canonically_ordered_comm_semiring._proof_10, bot := 0, bot_le := nat.zero_le, le_iff_exists_add := nat.canonically_ordered_comm_semiring._proof_11, mul := linear_ordered_semiring.mul infer_instance, mul_assoc := nat.canonically_ordered_comm_semiring._proof_12, one := linear_ordered_semiring.one infer_instance, one_mul := nat.canonically_ordered_comm_semiring._proof_13, mul_one := nat.canonically_ordered_comm_semiring._proof_14, zero_mul := nat.canonically_ordered_comm_semiring._proof_15, mul_zero := nat.canonically_ordered_comm_semiring._proof_16, left_distrib := nat.canonically_ordered_comm_semiring._proof_17, right_distrib := nat.canonically_ordered_comm_semiring._proof_18, mul_comm := nat.canonically_ordered_comm_semiring._proof_19, exists_pair_ne := _, eq_zero_or_eq_zero_of_mul_eq_zero := nat.canonically_ordered_comm_semiring._proof_20}

source

@[instance]

def nat.subtype.semilattice_sup_bot (s : set ℕ) [decidable_pred s] [h : nonempty ↥s] :

semilattice_sup_bot ↥s

Equations

nat.subtype.semilattice_sup_bot s = {bot := ⟨nat.find _, _⟩, le := linear_order.le (subtype.linear_order s), lt := linear_order.lt (subtype.linear_order s), le_refl := _, le_trans := _, lt_iff_le_not_le := _, le_antisymm := _, bot_le := _, sup := lattice.sup lattice_of_decidable_linear_order, le_sup_left := _, le_sup_right := _, sup_le := _}

source

theorem nat.mul_self_le_mul_self {n m : ℕ} :

n ≤ m → n * n ≤ m * m

source

theorem nat.mul_self_lt_mul_self {n m : ℕ} :

n < m → n * n < m * m

source

theorem nat.mul_self_le_mul_self_iff {n m : ℕ} :

n ≤ m ↔ n * n ≤ m * m

source

theorem nat.mul_self_lt_mul_self_iff {n m : ℕ} :

n < m ↔ n * n < m * m

source

theorem nat.le_mul_self (n : ℕ) :

n ≤ n * n

source

theorem nat.eq_of_mul_eq_mul_right {n m k : ℕ} :

0 < m → n * m = k * m → n = k

source

@[instance]

def nat.nat.comm_cancel_monoid_with_zero :

comm_cancel_monoid_with_zero ℕ

Equations

nat.nat.comm_cancel_monoid_with_zero = {mul := comm_monoid_with_zero.mul infer_instance, mul_assoc := nat.nat.comm_cancel_monoid_with_zero._proof_1, one := comm_monoid_with_zero.one infer_instance, one_mul := nat.nat.comm_cancel_monoid_with_zero._proof_2, mul_one := nat.nat.comm_cancel_monoid_with_zero._proof_3, mul_comm := nat.nat.comm_cancel_monoid_with_zero._proof_4, zero := comm_monoid_with_zero.zero infer_instance, zero_mul := nat.nat.comm_cancel_monoid_with_zero._proof_5, mul_zero := nat.nat.comm_cancel_monoid_with_zero._proof_6, mul_left_cancel_of_ne_zero := nat.nat.comm_cancel_monoid_with_zero._proof_7, mul_right_cancel_of_ne_zero := nat.nat.comm_cancel_monoid_with_zero._proof_8}

source

theorem nat.one_add (n : ℕ) :

1 + n = n.succ

source

@[simp]

theorem nat.add_def {a b : ℕ} :

a.add b = a + b

source

@[simp]

theorem nat.mul_def {a b : ℕ} :

a.mul b = a * b

source

@[simp]

theorem nat.succ_pos' {n : ℕ} :

0 < n.succ

source

theorem nat.succ_inj' {n m : ℕ} :

n.succ = m.succ ↔ n = m

source

theorem nat.succ_injective :

function.injective nat.succ

source

theorem nat.succ_le_succ_iff {m n : ℕ} :

m.succ ≤ n.succ ↔ m ≤ n

source

theorem nat.zero_max {m : ℕ} :

max 0 m = m

source

theorem nat.max_succ_succ {m n : ℕ} :

max m.succ n.succ = (max m n).succ

source

theorem nat.not_succ_lt_self {n : ℕ} :

¬n.succ < n

source

theorem nat.lt_succ_iff {m n : ℕ} :

m < n.succ ↔ m ≤ n

source

theorem nat.succ_le_iff {m n : ℕ} :

m.succ ≤ n ↔ m < n

source

theorem nat.lt_iff_add_one_le {m n : ℕ} :

m < n ↔ m + 1 ≤ n

source

theorem nat.lt_add_one_iff {a b : ℕ} :

a < b + 1 ↔ a ≤ b

source

theorem nat.lt_one_add_iff {a b : ℕ} :

a < 1 + b ↔ a ≤ b

source

theorem nat.add_one_le_iff {a b : ℕ} :

a + 1 ≤ b ↔ a < b

source

theorem nat.one_add_le_iff {a b : ℕ} :

1 + a ≤ b ↔ a < b

source

theorem nat.of_le_succ {n m : ℕ} :

n ≤ m.succ → n ≤ m ∨ n = m.succ

source

def nat.le_rec_on {C : ℕ → Sort u} {n m : ℕ} :

n ≤ m → (Π {k : ℕ}, C k → C (k + 1)) → C n → C m

Recursion starting at a non-zero number: given a map C k → C (k+1) for each k, there is a map from C n to each C m, n ≤ m.

Equations

nat.le_rec_on H next x = _.by_cases (λ (h : n ≤ m), next (nat.le_rec_on h next x)) (λ (h : n = m + 1), h.rec_on x)
nat.le_rec_on H next x = _.rec_on x

source

theorem nat.le_rec_on_self {C : ℕ → Sort u} {n : ℕ} {h : n ≤ n} {next : Π {k : ℕ}, C k → C (k + 1)} (x : C n) :

nat.le_rec_on h next x = x

source

theorem nat.le_rec_on_succ {C : ℕ → Sort u} {n m : ℕ} (h1 : n ≤ m) {h2 : n ≤ m + 1} {next : Π {k : ℕ}, C k → C (k + 1)} (x : C n) :

nat.le_rec_on h2 next x = next (nat.le_rec_on h1 next x)

source

theorem nat.le_rec_on_succ' {C : ℕ → Sort u} {n : ℕ} {h : n ≤ n + 1} {next : Π {k : ℕ}, C k → C (k + 1)} (x : C n) :

nat.le_rec_on h next x = next x

source

theorem nat.le_rec_on_trans {C : ℕ → Sort u} {n m k : ℕ} (hnm : n ≤ m) (hmk : m ≤ k) {next : Π {k : ℕ}, C k → C (k + 1)} (x : C n) :

nat.le_rec_on _ next x = nat.le_rec_on hmk next (nat.le_rec_on hnm next x)

source

theorem nat.le_rec_on_succ_left {C : ℕ → Sort u} {n m : ℕ} (h1 : n ≤ m) (h2 : n + 1 ≤ m) {next : Π ⦃k : ℕ⦄, C k → C (k + 1)} (x : C n) :

nat.le_rec_on h2 next (next x) = nat.le_rec_on h1 next x

source

theorem nat.le_rec_on_injective {C : ℕ → Sort u} {n m : ℕ} (hnm : n ≤ m) (next : Π (n : ℕ), C n → C (n + 1)) :

(∀ (n : ℕ), function.injective (next n)) → function.injective (nat.le_rec_on hnm next)

source

theorem nat.le_rec_on_surjective {C : ℕ → Sort u} {n m : ℕ} (hnm : n ≤ m) (next : Π (n : ℕ), C n → C (n + 1)) :

(∀ (n : ℕ), function.surjective (next n)) → function.surjective (nat.le_rec_on hnm next)

source

theorem nat.pred_eq_of_eq_succ {m n : ℕ} :

m = n.succ → m.pred = n

source

@[simp]

theorem nat.pred_eq_succ_iff {n m : ℕ} :

n.pred = m.succ ↔ n = m + 2

source

theorem nat.pred_sub (n m : ℕ) :

n.pred - m = (n - m).pred

source

@[simp]

theorem nat.add_succ_sub_one (n m : ℕ) :

n + m.succ - 1 = n + m

source

@[simp]

theorem nat.succ_add_sub_one (n m : ℕ) :

n.succ + m - 1 = n + m

source

theorem nat.pred_eq_sub_one (n : ℕ) :

n.pred = n - 1

source

theorem nat.one_le_of_lt {n m : ℕ} :

n < m → 1 ≤ m

source

theorem nat.le_pred_of_lt {n m : ℕ} :

m < n → m ≤ n - 1

source

theorem nat.le_of_pred_lt {m n : ℕ} :

m.pred < n → m ≤ n

source

@[simp]

theorem nat.pred_one_add (n : ℕ) :

(1 + n).pred = n

This ensures that simp succeeds on pred (n + 1) = n.

source

theorem nat.pos_iff_ne_zero {n : ℕ} :

0 < n ↔ n ≠ 0

source

theorem nat.one_lt_iff_ne_zero_and_ne_one {n : ℕ} :

1 < n ↔ n ≠ 0 ∧ n ≠ 1

source

theorem nat.eq_of_lt_succ_of_not_lt {a b : ℕ} :

a < b + 1 → ¬a < b → a = b

source

theorem nat.le_sub_add (n m : ℕ) :

n ≤ n - m + m

source

theorem nat.sub_add_eq_max (n m : ℕ) :

n - m + m = max n m

source

theorem nat.add_sub_eq_max (n m : ℕ) :

n + (m - n) = max n m

source

theorem nat.sub_add_min (n m : ℕ) :

n - m + min n m = n

source

theorem nat.add_sub_cancel' {n m : ℕ} :

m ≤ n → m + (n - m) = n

source

theorem nat.sub_eq_of_eq_add {m n k : ℕ} :

k = m + n → k - m = n

source

theorem nat.sub_cancel {a b c : ℕ} :

a ≤ b → a ≤ c → b - a = c - a → b = c

source

theorem nat.sub_sub_sub_cancel_right {a b c : ℕ} :

c ≤ b → a - c - (b - c) = a - b

source

theorem nat.add_sub_cancel_right (n m k : ℕ) :

n + (m + k) - k = n + m

source

theorem nat.sub_add_eq_add_sub {a b c : ℕ} :

b ≤ a → a - b + c = a + c - b

source

theorem nat.sub_min (n m : ℕ) :

n - min n m = n - m

source

theorem nat.sub_sub_assoc {a b c : ℕ} :

b ≤ a → c ≤ b → a - (b - c) = a - b + c

source

theorem nat.lt_of_sub_pos {m n : ℕ} :

0 < n - m → m < n

source

theorem nat.lt_of_sub_lt_sub_right {m n k : ℕ} :

m - k < n - k → m < n

source

theorem nat.lt_of_sub_lt_sub_left {m n k : ℕ} :

m - n < m - k → k < n

source

theorem nat.sub_lt_self {m n : ℕ} :

0 < m → 0 < n → m - n < m

source

theorem nat.le_sub_right_of_add_le {m n k : ℕ} :

m + k ≤ n → m ≤ n - k

source

theorem nat.le_sub_left_of_add_le {m n k : ℕ} :

k + m ≤ n → m ≤ n - k

source

theorem nat.lt_sub_right_of_add_lt {m n k : ℕ} :

m + k < n → m < n - k

source

theorem nat.lt_sub_left_of_add_lt {m n k : ℕ} :

k + m < n → m < n - k

source

theorem nat.add_lt_of_lt_sub_right {m n k : ℕ} :

m < n - k → m + k < n

source

theorem nat.add_lt_of_lt_sub_left {m n k : ℕ} :

m < n - k → k + m < n

source

theorem nat.le_add_of_sub_le_right {m n k : ℕ} :

n - k ≤ m → n ≤ m + k

source

theorem nat.le_add_of_sub_le_left {m n k : ℕ} :

n - k ≤ m → n ≤ k + m

source

theorem nat.lt_add_of_sub_lt_right {m n k : ℕ} :

n - k < m → n < m + k

source

theorem nat.lt_add_of_sub_lt_left {m n k : ℕ} :

n - k < m → n < k + m

source

theorem nat.sub_le_left_of_le_add {m n k : ℕ} :

n ≤ k + m → n - k ≤ m

source

theorem nat.sub_le_right_of_le_add {m n k : ℕ} :

n ≤ m + k → n - k ≤ m

source

theorem nat.sub_lt_left_iff_lt_add {m n k : ℕ} :

n ≤ k → (k - n < m ↔ k < n + m)

source

theorem nat.le_sub_left_iff_add_le {m n k : ℕ} :

m ≤ k → (n ≤ k - m ↔ m + n ≤ k)

source

theorem nat.le_sub_right_iff_add_le {m n k : ℕ} :

n ≤ k → (m ≤ k - n ↔ m + n ≤ k)

source

theorem nat.lt_sub_left_iff_add_lt {m n k : ℕ} :

n < k - m ↔ m + n < k

source

theorem nat.lt_sub_right_iff_add_lt {m n k : ℕ} :

m < k - n ↔ m + n < k

source

theorem nat.sub_le_left_iff_le_add {m n k : ℕ} :

m - n ≤ k ↔ m ≤ n + k

source

theorem nat.sub_le_right_iff_le_add {m n k : ℕ} :

m - k ≤ n ↔ m ≤ n + k

source

theorem nat.sub_lt_right_iff_lt_add {m n k : ℕ} :

k ≤ m → (m - k < n ↔ m < n + k)

source

theorem nat.sub_le_sub_left_iff {m n k : ℕ} :

k ≤ m → (m - n ≤ m - k ↔ k ≤ n)

source

theorem nat.sub_lt_sub_right_iff {m n k : ℕ} :

k ≤ m → (m - k < n - k ↔ m < n)

source

theorem nat.sub_lt_sub_left_iff {m n k : ℕ} :

n ≤ m → (m - n < m - k ↔ k < n)

source

theorem nat.sub_le_iff {m n k : ℕ} :

m - n ≤ k ↔ m - k ≤ n

source

theorem nat.sub_le_self (n m : ℕ) :

n - m ≤ n

source

theorem nat.sub_lt_iff {m n k : ℕ} :

n ≤ m → k ≤ m → (m - n < k ↔ m - k < n)

source

theorem nat.pred_le_iff {n m : ℕ} :

n.pred ≤ m ↔ n ≤ m.succ

source

theorem nat.lt_pred_iff {n m : ℕ} :

n < m.pred ↔ n.succ < m

source

theorem nat.lt_of_lt_pred {a b : ℕ} :

a < b - 1 → a < b

source

theorem nat.mul_ne_zero {n m : ℕ} :

n ≠ 0 → m ≠ 0 → n * m ≠ 0

source

@[simp]

theorem nat.mul_eq_zero {a b : ℕ} :

a * b = 0 ↔ a = 0 ∨ b = 0

source

@[simp]

theorem nat.zero_eq_mul {a b : ℕ} :

0 = a * b ↔ a = 0 ∨ b = 0

source

theorem nat.eq_zero_of_double_le {a : ℕ} :

2 * a ≤ a → a = 0

source

theorem nat.eq_zero_of_mul_le {a b : ℕ} :

2 ≤ b → b * a ≤ a → a = 0

source

theorem nat.le_mul_of_pos_left {m n : ℕ} :

0 < n → m ≤ n * m

source

theorem nat.le_mul_of_pos_right {m n : ℕ} :

0 < n → m ≤ m * n

source

theorem nat.two_mul_ne_two_mul_add_one {n m : ℕ} :

2 * n ≠ 2 * m + 1

source

def nat.strong_rec' {p : ℕ → Sort u} (H : Π (n : ℕ), (Π (m : ℕ), m < n → p m) → p n) (n : ℕ) :

p n

Recursion principle based on <.

Equations

nat.strong_rec' H n = H n (λ (m : ℕ) (hm : m < n), nat.strong_rec' H m)

source

def nat.strong_rec_on' {P : ℕ → Sort u_1} (n : ℕ) :

(Π (n : ℕ), (Π (m : ℕ), m < n → P m) → P n) → P n

Recursion principle based on < applied to some natural number.

Equations

n.strong_rec_on' h = nat.strong_rec' h n

source

theorem nat.strong_rec_on_beta' {P : ℕ → Sort u_1} {h : Π (n : ℕ), (Π (m : ℕ), m < n → P m) → P n} {n : ℕ} :

n.strong_rec_on' h = h n (λ (m : ℕ) (hmn : m < n), m.strong_rec_on' h)

source

theorem nat.div_le_of_le_mul' {m n k : ℕ} :

m ≤ k * n → m / k ≤ n

source

theorem nat.div_le_self' (m n : ℕ) :

m / n ≤ m

source

theorem nat.div_lt_self' (n b : ℕ) :

(n + 1) / (b + 2) < n + 1

A version of nat.div_lt_self using successors, rather than additional hypotheses.

source

theorem nat.le_div_iff_mul_le' {x y k : ℕ} :

0 < k → (x ≤ y / k ↔ x * k ≤ y)

source

theorem nat.div_mul_le_self' (m n : ℕ) :

m / n * n ≤ m

source

theorem nat.div_lt_iff_lt_mul' {x y k : ℕ} :

0 < k → (x / k < y ↔ x < y * k)

source

theorem nat.div_le_div_right {n m : ℕ} (h : n ≤ m) {k : ℕ} :

n / k ≤ m / k

source

theorem nat.lt_of_div_lt_div {m n k : ℕ} :

m / k < n / k → m < n

source

theorem nat.eq_mul_of_div_eq_right {a b c : ℕ} :

b ∣ a → a / b = c → a = b * c

source

theorem nat.div_eq_iff_eq_mul_right {a b c : ℕ} :

0 < b → b ∣ a → (a / b = c ↔ a = b * c)

source

theorem nat.div_eq_iff_eq_mul_left {a b c : ℕ} :

0 < b → b ∣ a → (a / b = c ↔ a = c * b)

source

theorem nat.eq_mul_of_div_eq_left {a b c : ℕ} :

b ∣ a → a / b = c → a = c * b

source

theorem nat.mul_div_cancel_left' {a b : ℕ} :

a ∣ b → a * (b / a) = b

source

theorem nat.div_mod_unique {n k m d : ℕ} :

0 < k → (n / k = d ∧ n % k = m ↔ m + k * d = n ∧ m < k)

source

theorem nat.two_mul_odd_div_two {n : ℕ} :

n % 2 = 1 → 2 * (n / 2) = n - 1

source

theorem nat.div_dvd_of_dvd {a b : ℕ} :

b ∣ a → a / b ∣ a

source

theorem nat.div_pos {a b : ℕ} :

b ≤ a → 0 < b → 0 < a / b

source

theorem nat.mul_left_inj {a b c : ℕ} :

0 < a → (b * a = c * a ↔ b = c)

source

theorem nat.mul_right_inj {a b c : ℕ} :

0 < a → (a * b = a * c ↔ b = c)

source

theorem nat.div_div_self {a b : ℕ} :

b ∣ a → 0 < a → a / (a / b) = b

source

theorem nat.div_lt_of_lt_mul {m n k : ℕ} :

m < n * k → m / n < k

source

theorem nat.lt_mul_of_div_lt {a b c : ℕ} :

a / c < b → 0 < c → a < b * c

source

theorem nat.div_eq_zero_iff {a b : ℕ} :

0 < b → (a / b = 0 ↔ a < b)

source

theorem nat.eq_zero_of_le_div {a b : ℕ} :

2 ≤ b → a ≤ a / b → a = 0

source

theorem nat.mul_div_le_mul_div_assoc (a b c : ℕ) :

a * (b / c) ≤ a * b / c

source

theorem nat.div_mul_div_le_div (a b c : ℕ) :

a / c * b / a ≤ b / c

source

theorem nat.eq_zero_of_le_half {a : ℕ} :

a ≤ a / 2 → a = 0

source

theorem nat.mod_mul_right_div_self (a b c : ℕ) :

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

source

theorem nat.mod_mul_left_div_self (a b c : ℕ) :

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

source

theorem nat.triangle_succ (n : ℕ) :

(n + 1) * (n + 1 - 1) / 2 = n * (n - 1) / 2 + n

source

@[simp]

theorem nat.dvd_one {n : ℕ} :

n ∣ 1 ↔ n = 1

source

theorem nat.dvd_add_left {k m n : ℕ} :

k ∣ n → (k ∣ m + n ↔ k ∣ m)

source

theorem nat.dvd_add_right {k m n : ℕ} :

k ∣ m → (k ∣ m + n ↔ k ∣ n)

source

@[simp]

theorem nat.not_two_dvd_bit1 (n : ℕ) :

¬2 ∣ bit1 n

source

@[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 b.

source

@[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 b.

source

theorem nat.mul_dvd_mul_iff_left {a b c : ℕ} :

0 < a → (a * b ∣ a * c ↔ b ∣ c)

source

theorem nat.mul_dvd_mul_iff_right {a b c : ℕ} :

0 < c → (a * c ∣ b * c ↔ a ∣ b)

source

theorem nat.succ_div (a b : ℕ) :

(a + 1) / b = a / b + ite (b ∣ a + 1) 1 0

source

theorem nat.succ_div_of_dvd {a b : ℕ} :

b ∣ a + 1 → (a + 1) / b = a / b + 1

source

theorem nat.succ_div_of_not_dvd {a b : ℕ} :

¬b ∣ a + 1 → (a + 1) / b = a / b

source

@[simp]

theorem nat.mod_mod_of_dvd (n : ℕ) {m k : ℕ} :

m ∣ k → n % k % m = n % m

source

@[simp]

theorem nat.mod_mod (a n : ℕ) :

a % n % n = a % n

source

theorem nat.sub_mod_eq_zero_of_mod_eq {a b c : ℕ} :

a % c = b % c → (a - b) % c = 0

If a and b are equal mod c, a - b is zero mod c.

source

@[simp]

theorem nat.one_mod (n : ℕ) :

1 % (n + 2) = 1

source

theorem nat.dvd_sub_mod {n : ℕ} (k : ℕ) :

n ∣ k - k % n

source

@[simp]

theorem nat.mod_add_mod (m n k : ℕ) :

(m % n + k) % n = (m + k) % n

source

@[simp]

theorem nat.add_mod_mod (m n k : ℕ) :

(m + n % k) % k = (m + n) % k

source

theorem nat.add_mod (a b n : ℕ) :

(a + b) % n = (a % n + b % n) % n

source

theorem nat.add_mod_eq_add_mod_right {m n k : ℕ} (i : ℕ) :

m % n = k % n → (m + i) % n = (k + i) % n

source

theorem nat.add_mod_eq_add_mod_left {m n k : ℕ} (i : ℕ) :

m % n = k % n → (i + m) % n = (i + k) % n

source

theorem nat.mul_mod (a b n : ℕ) :

a * b % n = a % n * (b % n) % n

source

theorem nat.add_pos_left {m : ℕ} (h : 0 < m) (n : ℕ) :

0 < m + n

source

theorem nat.add_pos_right (m : ℕ) {n : ℕ} :

0 < n → 0 < m + n

source

theorem nat.add_pos_iff_pos_or_pos (m n : ℕ) :

0 < m + n ↔ 0 < m ∨ 0 < n

source

theorem nat.add_eq_one_iff {a b : ℕ} :

a + b = 1 ↔ a = 0 ∧ b = 1 ∨ a = 1 ∧ b = 0

source

theorem nat.mul_eq_one_iff {a b : ℕ} :

a * b = 1 ↔ a = 1 ∧ b = 1

source

theorem nat.mul_right_eq_self_iff {a b : ℕ} :

0 < a → (a * b = a ↔ b = 1)

source

theorem nat.mul_left_eq_self_iff {a b : ℕ} :

0 < b → (a * b = b ↔ a = 1)

source

theorem nat.lt_succ_iff_lt_or_eq {n i : ℕ} :

n < i.succ ↔ n < i ∨ n = i

source

theorem nat.le_zero_iff {i : ℕ} :

i ≤ 0 ↔ i = 0

source

theorem nat.le_add_one_iff {i j : ℕ} :

i ≤ j + 1 ↔ i ≤ j ∨ i = j + 1

source

theorem nat.mul_self_inj {n m : ℕ} :

n * n = m * m ↔ n = m

source

@[instance]

def nat.succ_pos'' (n : ℕ) :

fact (0 < n.succ)

Equations

_ = _

source

@[instance]

def nat.pos_of_one_lt (n : ℕ) [h : fact (1 < n)] :

fact (0 < n)

Equations

_ = _

source

@[instance]

def nat.decidable_ball_lt (n : ℕ) (P : Π (k : ℕ), k < n → Prop) [H : Π (n_1 : ℕ) (h : n_1 < n), decidable (P n_1 h)] :

decidable (∀ (n_1 : ℕ) (h : n_1 < n), P n_1 h)

Equations

n.decidable_ball_lt P = nat.rec (λ (P : Π (k : ℕ), k < 0 → Prop) (H : Π (n : ℕ) (h : n < 0), decidable (P n h)), decidable.is_true _) (λ (n : ℕ) (IH : Π (P : Π (k : ℕ), k < n → Prop) [H : Π (n_1 : ℕ) (h : n_1 < n), decidable (P n_1 h)], decidable (∀ (n_1 : ℕ) (h : n_1 < n), P n_1 h)) (P : Π (k : ℕ), k < n.succ → Prop) (H : Π (n_1 : ℕ) (h : n_1 < n.succ), decidable (P n_1 h)), (IH (λ (k : ℕ) (h : k < n), P k _)).cases_on (λ (h : ¬∀ (n_1 : ℕ) (h : n_1 < n), (λ (k : ℕ) (h : k < n), P k _) n_1 h), decidable.is_false _) (λ (h : ∀ (n_1 : ℕ) (h : n_1 < n), (λ (k : ℕ) (h : k < n), P k _) n_1 h), dite (P n _) (λ (p : P n _), decidable.is_true _) (λ (p : ¬P n _), decidable.is_false _))) n P

source

@[instance]

def nat.decidable_forall_fin {n : ℕ} (P : fin n → Prop) [H : decidable_pred P] :

decidable (∀ (i : fin n), P i)

Equations

nat.decidable_forall_fin P = decidable_of_iff (∀ (k : ℕ) (h : k < n), P ⟨k, h⟩) _

source

@[instance]

def nat.decidable_ball_le (n : ℕ) (P : Π (k : ℕ), k ≤ n → Prop) [H : Π (n_1 : ℕ) (h : n_1 ≤ n), decidable (P n_1 h)] :

decidable (∀ (n_1 : ℕ) (h : n_1 ≤ n), P n_1 h)

Equations

n.decidable_ball_le P = decidable_of_iff (∀ (k : ℕ) (h : k < n.succ), P k _) _

source

@[instance]

def nat.decidable_lo_hi (lo hi : ℕ) (P : ℕ → Prop) [H : decidable_pred P] :

decidable (∀ (x : ℕ), lo ≤ x → x < hi → P x)

Equations

lo.decidable_lo_hi hi P = decidable_of_iff (∀ (x : ℕ), x < hi - lo → P (lo + x)) _

source

@[instance]

def nat.decidable_lo_hi_le (lo hi : ℕ) (P : ℕ → Prop) [H : decidable_pred P] :

decidable (∀ (x : ℕ), lo ≤ x → x ≤ hi → P x)

Equations

lo.decidable_lo_hi_le hi P = decidable_of_iff (∀ (x : ℕ), lo ≤ x → x < hi + 1 → P x) _

source

theorem nat.bit0_le {n m : ℕ} :

n ≤ m → bit0 n ≤ bit0 m

source

theorem nat.bit1_le {n m : ℕ} :

n ≤ m → bit1 n ≤ bit1 m

source

theorem nat.bit_le (b : bool) {n m : ℕ} :

n ≤ m → nat.bit b n ≤ nat.bit b m

source

theorem nat.bit_ne_zero (b : bool) {n : ℕ} :

n ≠ 0 → nat.bit b n ≠ 0

source

theorem nat.bit0_le_bit (b : bool) {m n : ℕ} :

m ≤ n → bit0 m ≤ nat.bit b n

source

theorem nat.bit_le_bit1 (b : bool) {m n : ℕ} :

m ≤ n → nat.bit b m ≤ bit1 n

source

theorem nat.bit_lt_bit0 (b : bool) {n m : ℕ} :

n < m → nat.bit b n < bit0 m

source

theorem nat.bit_lt_bit (a b : bool) {n m : ℕ} :

n < m → nat.bit a n < nat.bit b m

source

@[simp]

theorem nat.bit0_le_bit1_iff {n k : ℕ} :

bit0 k ≤ bit1 n ↔ k ≤ n

source

@[simp]

theorem nat.bit0_lt_bit1_iff {n k : ℕ} :

bit0 k < bit1 n ↔ k ≤ n

source

@[simp]

theorem nat.bit1_le_bit0_iff {n k : ℕ} :

bit1 k ≤ bit0 n ↔ k < n

source

@[simp]

theorem nat.bit1_lt_bit0_iff {n k : ℕ} :

bit1 k < bit0 n ↔ k < n

source

@[simp]

theorem nat.one_le_bit0_iff {n : ℕ} :

1 ≤ bit0 n ↔ 0 < n

source

@[simp]

theorem nat.one_lt_bit0_iff {n : ℕ} :

1 < bit0 n ↔ 1 ≤ n

source

@[simp]

theorem nat.bit_le_bit_iff {n k : ℕ} {b : bool} :

nat.bit b k ≤ nat.bit b n ↔ k ≤ n

source

@[simp]

theorem nat.bit_lt_bit_iff {n k : ℕ} {b : bool} :

nat.bit b k < nat.bit b n ↔ k < n

source

@[simp]

theorem nat.bit_le_bit1_iff {n k : ℕ} {b : bool} :

nat.bit b k ≤ bit1 n ↔ k ≤ n

source

theorem nat.pos_of_bit0_pos {n : ℕ} :

0 < bit0 n → 0 < n

source

def nat.bit_cases {C : ℕ → Sort u} (H : Π (b : bool) (n : ℕ), C (nat.bit b n)) (n : ℕ) :

C n

Define a function on ℕ depending on parity of the argument.

Equations

nat.bit_cases H n = _.rec_on (H n.bodd n.div2)

source

@[simp]

def nat.ppred :

ℕ → option ℕ

Partial predecessor operation. Returns ppred n = some m if n = m + 1, otherwise none.

Equations

(n + 1).ppred = option.some n
0.ppred = option.none

source

@[simp]

def nat.psub :

ℕ → ℕ → option ℕ

Partial subtraction operation. Returns psub m n = some k if m = n + k, otherwise none.

Equations

m.psub (n + 1) = m.psub n >>= nat.ppred
m.psub 0 = option.some m

source

theorem nat.pred_eq_ppred (n : ℕ) :

n.pred = n.ppred.get_or_else 0

source

theorem nat.sub_eq_psub (m n : ℕ) :

m - n = (m.psub n).get_or_else 0

source

@[simp]

theorem nat.ppred_eq_some {m n : ℕ} :

n.ppred = option.some m ↔ m.succ = n

source

@[simp]

theorem nat.ppred_eq_none {n : ℕ} :

n.ppred = option.none ↔ n = 0

source

theorem nat.psub_eq_some {m n k : ℕ} :

m.psub n = option.some k ↔ k + n = m

source

theorem nat.psub_eq_none (m n : ℕ) :

m.psub n = option.none ↔ m < n

source

theorem nat.ppred_eq_pred {n : ℕ} :

0 < n → n.ppred = option.some n.pred

source

theorem nat.psub_eq_sub {m n : ℕ} :

n ≤ m → m.psub n = option.some (m - n)

source

theorem nat.psub_add (m n k : ℕ) :

m.psub (n + k) = m.psub n >>= λ (x : ℕ), x.psub k

source

@[simp]

theorem nat.one_pow (n : ℕ) :

1 ^ n = 1

source

theorem nat.pow_add (a m n : ℕ) :

a ^ (m + n) = a ^ m * a ^ n

source

theorem nat.pow_two (a : ℕ) :

a ^ 2 = a * a

source

theorem nat.pow_dvd_pow (a : ℕ) {m n : ℕ} :

m ≤ n → a ^ m ∣ a ^ n

source

theorem nat.pow_dvd_pow_of_dvd {a b : ℕ} (h : a ∣ b) (n : ℕ) :

a ^ n ∣ b ^ n

source

theorem nat.mul_pow (a b n : ℕ) :

(a * b) ^ n = a ^ n * b ^ n

source

theorem nat.pow_mul (a b n : ℕ) :

n ^ (a * b) = (n ^ a) ^ b

source

theorem nat.pow_pos {p : ℕ} (hp : 0 < p) (n : ℕ) :

0 < p ^ n

source

theorem nat.pow_eq_mul_pow_sub (p : ℕ) {m n : ℕ} :

m ≤ n → p ^ m * p ^ (n - m) = p ^ n

source

theorem nat.pow_lt_pow_succ {p : ℕ} (h : 1 < p) (n : ℕ) :

p ^ n < p ^ (n + 1)

source

theorem nat.lt_pow_self {p : ℕ} (h : 1 < p) (n : ℕ) :

n < p ^ n

source

theorem nat.lt_two_pow (n : ℕ) :

n < 2 ^ n

source

theorem nat.one_le_pow (n m : ℕ) :

0 < m → 1 ≤ m ^ n

source

theorem nat.one_le_pow' (n m : ℕ) :

1 ≤ (m + 1) ^ n

source

theorem nat.one_le_two_pow (n : ℕ) :

1 ≤ 2 ^ n

source

theorem nat.one_lt_pow (n m : ℕ) :

0 < n → 1 < m → 1 < m ^ n

source

theorem nat.one_lt_pow' (n m : ℕ) :

1 < (m + 2) ^ (n + 1)

source

theorem nat.one_lt_two_pow (n : ℕ) :

0 < n → 1 < 2 ^ n

source

theorem nat.one_lt_two_pow' (n : ℕ) :

1 < 2 ^ (n + 1)

source

theorem nat.pow_right_strict_mono {x : ℕ} :

2 ≤ x → strict_mono x.pow

source

theorem nat.pow_le_iff_le_right {x m n : ℕ} :

2 ≤ x → (x ^ m ≤ x ^ n ↔ m ≤ n)

source

theorem nat.pow_lt_iff_lt_right {x m n : ℕ} :

2 ≤ x → (x ^ m < x ^ n ↔ m < n)

source

theorem nat.pow_right_injective {x : ℕ} :

2 ≤ x → function.injective x.pow

source

theorem nat.pow_dvd_pow_iff_pow_le_pow {k l x : ℕ} :

0 < x → (x ^ k ∣ x ^ l ↔ x ^ k ≤ x ^ l)

source

theorem nat.pow_dvd_pow_iff_le_right {x k l : ℕ} :

1 < x → (x ^ k ∣ x ^ l ↔ k ≤ l)

If 1 < x, then x^k divides x^l if and only if k is at most l.

source

theorem nat.pow_dvd_pow_iff_le_right' {b k l : ℕ} :

(b + 2) ^ k ∣ (b + 2) ^ l ↔ k ≤ l

source

theorem nat.pow_left_strict_mono {m : ℕ} :

1 ≤ m → strict_mono (λ (x : ℕ), x ^ m)

source

theorem nat.pow_le_iff_le_left {m x y : ℕ} :

1 ≤ m → (x ^ m ≤ y ^ m ↔ x ≤ y)

source

theorem nat.pow_lt_iff_lt_left {m x y : ℕ} :

1 ≤ m → (x ^ m < y ^ m ↔ x < y)

source

theorem nat.pow_left_injective {m : ℕ} :

1 ≤ m → function.injective (λ (x : ℕ), x ^ m)

source

theorem nat.not_pos_pow_dvd {p k : ℕ} :

1 < p → 1 < k → ¬p ^ k ∣ p

source

@[simp]

theorem nat.bodd_div2_eq (n : ℕ) :

n.bodd_div2 = (n.bodd, n.div2)

source

@[simp]

theorem nat.bodd_bit0 (n : ℕ) :

(bit0 n).bodd = bool.ff

source

@[simp]

theorem nat.bodd_bit1 (n : ℕ) :

(bit1 n).bodd = bool.tt

source

@[simp]

theorem nat.div2_bit0 (n : ℕ) :

(bit0 n).div2 = n

source

@[simp]

theorem nat.div2_bit1 (n : ℕ) :

(bit1 n).div2 = n

source

theorem nat.shiftl'_ne_zero_left (b : bool) {m : ℕ} (h : m ≠ 0) (n : ℕ) :

nat.shiftl' b m n ≠ 0

source

theorem nat.shiftl'_tt_ne_zero (m : ℕ) {n : ℕ} :

n ≠ 0 → nat.shiftl' bool.tt m n ≠ 0

source

@[simp]

theorem nat.size_zero :

0.size = 0

source

@[simp]

theorem nat.size_bit {b : bool} {n : ℕ} :

nat.bit b n ≠ 0 → (nat.bit b n).size = n.size.succ

source

@[simp]

theorem nat.size_bit0 {n : ℕ} :

n ≠ 0 → (bit0 n).size = n.size.succ

source

@[simp]

theorem nat.size_bit1 (n : ℕ) :

(bit1 n).size = n.size.succ

source

@[simp]

theorem nat.size_one :

1.size = 1

source

@[simp]

theorem nat.size_shiftl' {b : bool} {m n : ℕ} :

nat.shiftl' b m n ≠ 0 → (nat.shiftl' b m n).size = m.size + n

source

@[simp]

theorem nat.size_shiftl {m : ℕ} (h : m ≠ 0) (n : ℕ) :

(m.shiftl n).size = m.size + n

source

theorem nat.lt_size_self (n : ℕ) :

n < 2 ^ n.size

source

theorem nat.size_le {m n : ℕ} :

m.size ≤ n ↔ m < 2 ^ n

source

theorem nat.lt_size {m n : ℕ} :

m < n.size ↔ 2 ^ m ≤ n

source

theorem nat.size_pos {n : ℕ} :

0 < n.size ↔ 0 < n

source

theorem nat.size_eq_zero {n : ℕ} :

n.size = 0 ↔ n = 0

source

theorem nat.size_pow {n : ℕ} :

(2 ^ n).size = n + 1

source

theorem nat.size_le_size {m n : ℕ} :

m ≤ n → m.size ≤ n.size

source

@[simp]

def nat.fact :

ℕ → ℕ

fact n is the factorial of n.

Equations

n.succ.fact = n.succ * n.fact
0.fact = 1

source

@[simp]

theorem nat.fact_zero :

0.fact = 1

source

@[simp]

theorem nat.fact_succ (n : ℕ) :

n.succ.fact = n.succ * n.fact

source

@[simp]

theorem nat.fact_one :

1.fact = 1

source

theorem nat.fact_pos (n : ℕ) :

0 < n.fact

source

theorem nat.fact_ne_zero (n : ℕ) :

n.fact ≠ 0

source

theorem nat.fact_dvd_fact {m n : ℕ} :

m ≤ n → m.fact ∣ n.fact

source

theorem nat.dvd_fact {m n : ℕ} :

0 < m → m ≤ n → m ∣ n.fact

source

theorem nat.fact_le {m n : ℕ} :

m ≤ n → m.fact ≤ n.fact

source

theorem nat.fact_mul_pow_le_fact {m n : ℕ} :

m.fact * m.succ ^ n ≤ (m + n).fact

source

theorem nat.monotone_fact :

monotone nat.fact

source

theorem nat.fact_lt {m n : ℕ} :

0 < n → (n.fact < m.fact ↔ n < m)

source

theorem nat.one_lt_fact {n : ℕ} :

1 < n.fact ↔ 1 < n

source

theorem nat.fact_eq_one {n : ℕ} :

n.fact = 1 ↔ n ≤ 1

source

theorem nat.fact_inj {m n : ℕ} :

1 < n.fact → (n.fact = m.fact ↔ n = m)

source

def nat.choose :

ℕ → ℕ → ℕ

choose n k is the number of k-element subsets in an n-element set. Also known as binomial coefficients.

Equations

(n + 1).choose (k + 1) = n.choose k + n.choose (k + 1)
n.succ.choose 0 = 1
0.choose (k + 1) = 0
0.choose 0 = 1

source

@[simp]

theorem nat.choose_zero_right (n : ℕ) :

n.choose 0 = 1

source

@[simp]

theorem nat.choose_zero_succ (k : ℕ) :

0.choose k.succ = 0

source

theorem nat.choose_succ_succ (n k : ℕ) :

n.succ.choose k.succ = n.choose k + n.choose k.succ

source

theorem nat.choose_eq_zero_of_lt {n k : ℕ} :

n < k → n.choose k = 0

source

@[simp]

theorem nat.choose_self (n : ℕ) :

n.choose n = 1

source

@[simp]

theorem nat.choose_succ_self (n : ℕ) :

n.choose n.succ = 0

source

@[simp]

theorem nat.choose_one_right (n : ℕ) :

n.choose 1 = n

source

theorem nat.choose_two_right (n : ℕ) :

n.choose 2 = n * (n - 1) / 2

choose n 2 is the n-th triangle number.

source

theorem nat.choose_pos {n k : ℕ} :

k ≤ n → 0 < n.choose k

source

theorem nat.succ_mul_choose_eq (n k : ℕ) :

n.succ * n.choose k = n.succ.choose k.succ * k.succ

source

theorem nat.choose_mul_fact_mul_fact {n k : ℕ} :

k ≤ n → n.choose k * k.fact * (n - k).fact = n.fact

source

theorem nat.choose_eq_fact_div_fact {n k : ℕ} :

k ≤ n → n.choose k = n.fact / (k.fact * (n - k).fact)

source

theorem nat.fact_mul_fact_dvd_fact {n k : ℕ} :

k ≤ n → k.fact * (n - k).fact ∣ n.fact

source

@[simp]

theorem nat.choose_symm {n k : ℕ} :

k ≤ n → n.choose (n - k) = n.choose k

source

theorem nat.choose_symm_of_eq_add {n a b : ℕ} :

n = a + b → n.choose a = n.choose b

source

theorem nat.choose_symm_add {a b : ℕ} :

(a + b).choose a = (a + b).choose b

source

theorem nat.choose_symm_half (m : ℕ) :

(2 * m + 1).choose (m + 1) = (2 * m + 1).choose m

source

theorem nat.choose_succ_right_eq (n k : ℕ) :

n.choose (k + 1) * (k + 1) = n.choose k * (n - k)

source

@[simp]

theorem nat.choose_succ_self_right (n : ℕ) :

(n + 1).choose n = n + 1

source

theorem nat.choose_mul_succ_eq (n k : ℕ) :

n.choose k * (n + 1) = (n + 1).choose k * (n + 1 - k)

source

theorem nat.units_eq_one (u : units ℕ) :

u = 1

source

theorem nat.add_units_eq_zero (u : add_units ℕ) :

u = 0

source

@[simp]

theorem nat.is_unit_iff {n : ℕ} :

is_unit n ↔ n = 1

source

@[simp]

theorem nat.find_eq_zero {p : ℕ → Prop} [decidable_pred p] (h : ∃ (n : ℕ), p n) :

nat.find h = 0 ↔ p 0

source

@[simp]

theorem nat.find_pos {p : ℕ → Prop} [decidable_pred p] (h : ∃ (n : ℕ), p n) :

0 < nat.find h ↔ ¬p 0

source

def nat.find_greatest (P : ℕ → Prop) [decidable_pred P] :

ℕ → ℕ

find_greatest P b is the largest i ≤ bound such that P i holds, or 0 if no such i exists

Equations

nat.find_greatest P (n + 1) = ite (P (n + 1)) (n + 1) (nat.find_greatest P n)
nat.find_greatest P 0 = 0

source

@[simp]

theorem nat.find_greatest_zero {P : ℕ → Prop} [decidable_pred P] :

nat.find_greatest P 0 = 0

source

@[simp]

theorem nat.find_greatest_eq {P : ℕ → Prop} [decidable_pred P] {b : ℕ} :

P b → nat.find_greatest P b = b

source

@[simp]

theorem nat.find_greatest_of_not {P : ℕ → Prop} [decidable_pred P] {b : ℕ} :

¬P (b + 1) → nat.find_greatest P (b + 1) = nat.find_greatest P b

source

theorem nat.find_greatest_spec_and_le {P : ℕ → Prop} [decidable_pred P] {b m : ℕ} :

m ≤ b → P m → P (nat.find_greatest P b) ∧ m ≤ nat.find_greatest P b

source

theorem nat.find_greatest_spec {P : ℕ → Prop} [decidable_pred P] {b : ℕ} :

(∃ (m : ℕ), m ≤ b ∧ P m) → P (nat.find_greatest P b)

source

theorem nat.find_greatest_le {P : ℕ → Prop} [decidable_pred P] {b : ℕ} :

nat.find_greatest P b ≤ b

source

theorem nat.le_find_greatest {P : ℕ → Prop} [decidable_pred P] {b m : ℕ} :

m ≤ b → P m → m ≤ nat.find_greatest P b

source

theorem nat.find_greatest_is_greatest {P : ℕ → Prop} [decidable_pred P] {b : ℕ} (a : ∃ (m : ℕ), m ≤ b ∧ P m) (k : ℕ) :

nat.find_greatest P b < k ∧ k ≤ b → ¬P k

source

theorem nat.find_greatest_eq_zero {P : ℕ → Prop} [decidable_pred P] {b : ℕ} :

(∀ (n : ℕ), n ≤ b → ¬P n) → nat.find_greatest P b = 0

source

theorem nat.find_greatest_of_ne_zero {P : ℕ → Prop} [decidable_pred P] {b m : ℕ} :

nat.find_greatest P b = m → m ≠ 0 → P m

source

theorem nat.dvd_div_of_mul_dvd {a b c : ℕ} :

a * b ∣ c → b ∣ c / a

source

theorem nat.mul_dvd_of_dvd_div {a b c : ℕ} :

c ∣ b → a ∣ b / c → c * a ∣ b

source

theorem nat.div_mul_div {a b c d : ℕ} :

b ∣ a → d ∣ c → a / b * (c / d) = a * c / (b * d)

source

@[simp]

theorem nat.div_div_div_eq_div {a b c : ℕ} :

b ∣ a → a ∣ c → c / (a / b) / b = c / a

source

theorem nat.pow_dvd_of_le_of_pow_dvd {p m n k : ℕ} :

m ≤ n → p ^ n ∣ k → p ^ m ∣ k

source

theorem nat.dvd_of_pow_dvd {p k m : ℕ} :

1 ≤ k → p ^ k ∣ m → p ∣ m

source

theorem nat.eq_of_dvd_of_div_eq_one {a b : ℕ} :

a ∣ b → b / a = 1 → a = b

source

theorem nat.eq_zero_of_dvd_of_div_eq_zero {a b : ℕ} :

a ∣ b → b / a = 0 → b = 0

source

theorem nat.eq_zero_of_dvd_of_lt {a b : ℕ} :

a ∣ b → b < a → b = 0

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

source

theorem nat.div_le_div_left {a b c : ℕ} :

c ≤ b → 0 < c → a / b ≤ a / c

source

theorem nat.div_eq_self {a b : ℕ} :

a / b = a ↔ a = 0 ∨ b = 1

source

theorem nat.exists_eq_add_of_le {m n : ℕ} :

m ≤ n → (∃ (k : ℕ), n = m + k)

source

theorem nat.exists_eq_add_of_lt {m n : ℕ} :

m < n → (∃ (k : ℕ), n = m + k + 1)

source

theorem nat.with_bot.add_eq_zero_iff {n m : with_bot ℕ} :

n + m = 0 ↔ n = 0 ∧ m = 0

source

theorem nat.with_bot.add_eq_one_iff {n m : with_bot ℕ} :

n + m = 1 ↔ n = 0 ∧ m = 1 ∨ n = 1 ∧ m = 0

source

@[simp]

theorem nat.with_bot.coe_nonneg {n : ℕ} :

0 ≤ ↑n

source

@[simp]

theorem nat.with_bot.lt_zero_iff (n : with_bot ℕ) :

n < 0 ↔ n = ⊥

source

theorem nat.le_induction {P : ℕ → Prop} {m : ℕ} (h0 : P m) (h1 : ∀ (n : ℕ), m ≤ n → P n → P (n + 1)) (n : ℕ) :

m ≤ n → P n

Induction principle starting at a non-zero number. For maps to a Sort* see le_rec_on.

source

def nat.decreasing_induction {P : ℕ → Sort u_1} (h : Π (n : ℕ), P (n + 1) → P n) {m n : ℕ} :

m ≤ n → P n → P m

Decreasing induction: if P (k+1) implies P k, then P n implies P m for all m ≤ n. Also works for functions to Sort*.

Equations

nat.decreasing_induction h mn hP = nat.le_rec_on mn (λ (k : ℕ) (ih : P k → P m) (hsk : P (k + 1)), ih (h k hsk)) (λ (h : P m), h) hP

source

@[simp]

theorem nat.decreasing_induction_self {P : ℕ → Sort u_1} (h : Π (n : ℕ), P (n + 1) → P n) {n : ℕ} (nn : n ≤ n) (hP : P n) :

nat.decreasing_induction h nn hP = hP

source

theorem nat.decreasing_induction_succ {P : ℕ → Sort u_1} (h : Π (n : ℕ), P (n + 1) → P n) {m n : ℕ} (mn : m ≤ n) (msn : m ≤ n + 1) (hP : P (n + 1)) :

nat.decreasing_induction h msn hP = nat.decreasing_induction h mn (h n hP)

source

@[simp]

theorem nat.decreasing_induction_succ' {P : ℕ → Sort u_1} (h : Π (n : ℕ), P (n + 1) → P n) {m : ℕ} (msm : m ≤ m + 1) (hP : P (m + 1)) :

nat.decreasing_induction h msm hP = h m hP

source

theorem nat.decreasing_induction_trans {P : ℕ → Sort u_1} (h : Π (n : ℕ), P (n + 1) → P n) {m n k : ℕ} (mn : m ≤ n) (nk : n ≤ k) (hP : P k) :

nat.decreasing_induction h _ hP = nat.decreasing_induction h mn (nat.decreasing_induction h nk hP)

source

theorem nat.decreasing_induction_succ_left {P : ℕ → Sort u_1} (h : Π (n : ℕ), P (n + 1) → P n) {m n : ℕ} (smn : m + 1 ≤ n) (mn : m ≤ n) (hP : P n) :

nat.decreasing_induction h mn hP = h m (nat.decreasing_induction h smn hP)

source

def nat.log :

ℕ → ℕ → ℕ

log b n, is the logarithm of natural number n in base b. It returns the largest k:ℕ such that b^k ≤ n, so if b^k = n, it returns exactly k.

Equations

b.log n = ite (b ≤ n ∧ 1 < b) (b.log (n / b) + 1) 0

source

theorem nat.pow_le_iff_le_log (x y : ℕ) {b : ℕ} :

1 < b → 1 ≤ y → (b ^ x ≤ y ↔ x ≤ b.log y)

source

theorem nat.log_pow (b x : ℕ) :

1 < b → b.log (b ^ x) = x

source

theorem nat.pow_succ_log_gt_self (b x : ℕ) :

1 < b → 1 ≤ x → x < b ^ (b.log x).succ

source

theorem nat.pow_log_le_self (b x : ℕ) :

1 < b → 1 ≤ x → b ^ b.log x ≤ x

mathlib documentation

data.nat.basic

Basic operations on the natural numbers

General documentation

Additional documentation

Library

mathlib documentation

data.​nat.​basic

Basic operations on the natural numbers

General documentation

Additional documentation

Library

data.nat.basic