mathlib docs: core.init.data.nat.basic

source

inductive nat.less_than_or_equal :

ℕ → ℕ → Prop

refl : ∀ (a : ℕ), a.less_than_or_equal a
step : ∀ (a : ℕ) {b : ℕ}, a.less_than_or_equal b → a.less_than_or_equal b.succ

source

@[instance]

def nat.has_le :

has_le ℕ

Equations

nat.has_le = {le := nat.less_than_or_equal}

source

def nat.le :

ℕ → ℕ → Prop

Equations

n.le m = n.less_than_or_equal m

source

def nat.lt :

ℕ → ℕ → Prop

Equations

n.lt m = n.succ.less_than_or_equal m

source

@[instance]

def nat.has_lt :

has_lt ℕ

Equations

nat.has_lt = {lt := nat.lt}

source

def nat.pred :

ℕ → ℕ

Equations

(a + 1).pred = a
0.pred = 0

source

def nat.sub :

ℕ → ℕ → ℕ

Equations

a.sub (b + 1) = (a.sub b).pred
a.sub 0 = a

source

def nat.mul :

ℕ → ℕ → ℕ

Equations

a.mul (b + 1) = a.mul b + a
a.mul 0 = 0

source

@[instance]

def nat.has_sub :

has_sub ℕ

Equations

nat.has_sub = {sub := nat.sub}

source

@[instance]

def nat.has_mul :

has_mul ℕ

Equations

nat.has_mul = {mul := nat.mul}

source

@[instance]

def nat.has_dvd :

has_dvd ℕ

Equations

nat.has_dvd = {dvd := λ (a b : ℕ), ∃ (c : ℕ), b = a * c}

source

@[instance]

def nat.decidable_eq :

decidable_eq ℕ

Equations

nat.decidable_eq x.succ y.succ = nat.decidable_eq._match_1 x y (nat.decidable_eq x y)
nat.decidable_eq x.succ 0 = decidable.is_false _
nat.decidable_eq 0 y.succ = decidable.is_false _
nat.decidable_eq 0 0 = decidable.is_true rfl
nat.decidable_eq._match_1 x y (decidable.is_true xeqy) = decidable.is_true _
nat.decidable_eq._match_1 x y (decidable.is_false xney) = decidable.is_false _

source

def nat.repeat {α : Type u} :

(ℕ → α → α) → ℕ → α → α

Equations

nat.repeat f n.succ a = f n (nat.repeat f n a)
nat.repeat f 0 a = a

source

@[instance]

def nat.inhabited :

inhabited ℕ

Equations

nat.inhabited = {default := 0}

source

@[simp]

theorem nat.nat_zero_eq_zero :

0 = 0

source

def nat.le_refl (a : ℕ) :

a ≤ a

Equations

_ = nat.less_than_or_equal.refl

source

theorem nat.le_succ (n : ℕ) :

n ≤ n.succ

source

theorem nat.succ_le_succ {n m : ℕ} :

n ≤ m → n.succ ≤ m.succ

source

theorem nat.zero_le (n : ℕ) :

0 ≤ n

source

theorem nat.zero_lt_succ (n : ℕ) :

0 < n.succ

source

def nat.succ_pos (n : ℕ) :

0 < n.succ

Equations

nat.succ_pos = nat.zero_lt_succ

source

theorem nat.not_succ_le_zero (n : ℕ) :

n.succ ≤ 0 → false

source

theorem nat.not_lt_zero (a : ℕ) :

¬a < 0

source

theorem nat.pred_le_pred {n m : ℕ} :

n ≤ m → n.pred ≤ m.pred

source

theorem nat.le_of_succ_le_succ {n m : ℕ} :

n.succ ≤ m.succ → n ≤ m

source

@[instance]

def nat.decidable_le (a b : ℕ) :

decidable (a ≤ b)

Equations

(a + 1).decidable_le (b + 1) = nat.decidable_le._match_1 a b (a.decidable_le b)
(a + 1).decidable_le 0 = decidable.is_false _
0.decidable_le b = decidable.is_true _
nat.decidable_le._match_1 a b (decidable.is_true h) = decidable.is_true _
nat.decidable_le._match_1 a b (decidable.is_false h) = decidable.is_false _

source

@[instance]

def nat.decidable_lt (a b : ℕ) :

decidable (a < b)

Equations

nat.decidable_lt = λ (a b : ℕ), a.succ.decidable_le b

source

theorem nat.eq_or_lt_of_le {a b : ℕ} :

a ≤ b → a = b ∨ a < b

source

theorem nat.lt_succ_of_le {a b : ℕ} :

a ≤ b → a < b.succ

source

@[simp]

theorem nat.succ_sub_succ_eq_sub (a b : ℕ) :

a.succ - b.succ = a - b

source

theorem nat.not_succ_le_self (n : ℕ) :

¬n.succ ≤ n

source

theorem nat.lt_irrefl (n : ℕ) :

¬n < n

source

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

n ≤ m → m ≤ k → n ≤ k

source

theorem nat.pred_le (n : ℕ) :

n.pred ≤ n

source

theorem nat.pred_lt {n : ℕ} :

n ≠ 0 → n.pred < n

source

theorem nat.sub_le (a b : ℕ) :

a - b ≤ a

source

theorem nat.sub_lt {a b : ℕ} :

0 < a → 0 < b → a - b < a

source

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

n < m → m ≤ k → n < k

source

theorem nat.zero_add (n : ℕ) :

0 + n = n

source

theorem nat.succ_add (n m : ℕ) :

n.succ + m = (n + m).succ

source

theorem nat.add_succ (n m : ℕ) :

n + m.succ = (n + m).succ

source

theorem nat.add_zero (n : ℕ) :

n + 0 = n

source

theorem nat.add_one (n : ℕ) :

n + 1 = n.succ

source

theorem nat.succ_eq_add_one (n : ℕ) :

n.succ = n + 1

source

theorem nat.bit0_succ_eq (n : ℕ) :

bit0 n.succ = (bit0 n).succ.succ

source

theorem nat.zero_lt_bit0 {n : ℕ} :

n ≠ 0 → 0 < bit0 n

source

theorem nat.zero_lt_bit1 (n : ℕ) :

0 < bit1 n

source

theorem nat.bit0_ne_zero {n : ℕ} :

n ≠ 0 → bit0 n ≠ 0

source

theorem nat.bit1_ne_zero (n : ℕ) :

bit1 n ≠ 0

source

def nat.pow :

ℕ → ℕ → ℕ

Equations

b.pow n.succ = b.pow n * b
b.pow 0 = 1

source

@[instance]

def nat.has_pow :

has_pow ℕ ℕ

Equations

nat.has_pow = {pow := nat.pow}

source

theorem nat.pow_succ (b n : ℕ) :

b ^ n.succ = b ^ n * b

source

@[simp]

theorem nat.pow_zero (b : ℕ) :

b ^ 0 = 1

mathlib documentation

core.init.data.nat.basic

General documentation

Additional documentation

Library

mathlib documentation

core.​init.​data.​nat.​basic

General documentation

Additional documentation

Library

core.init.data.nat.basic