Documentation

Init.Data.Nat.Basic

source
@[specialize]
def Nat.foldAux {α : Type u} (f : Nat → α → α) (s : Nat) :
Nat → α → α
Equations
source
@[inline]
def Nat.fold {α : Type u} (f : Nat → α → α) (n : Nat) (init : α) :
α
Equations
source
@[inline]
def Nat.foldRev {α : Type u} (f : Nat → α → α) (n : Nat) (init : α) :
α
Equations
source
@[specialize]
def Nat.foldRev.loop {α : Type u} (f : Nat → α → α) :
Nat → α → α
Equations
source
@[specialize]
def Nat.anyAux (f : Nat → Bool) (s : Nat) :
Nat → Bool
Equations
source
@[inline]
def Nat.any (f : Nat → Bool) (n : Nat) :
Bool
Equations
source
@[inline]
def Nat.all (f : Nat → Bool) (n : Nat) :
Bool
Equations
source
@[inline]
def Nat.repeat {α : Type u} (f : α → α) (n : Nat) (a : α) :
α
Equations
source
@[specialize]
def Nat.repeat.loop {α : Type u} (f : α → α) :
Nat → α → α
Equations
source
@[simp]
theorem Nat.zero_eq :
Nat.zero = 0
source
@[simp]
theorem Nat.add_eq {x : Nat} {y : Nat} :
Nat.add x y = x + y
source
@[simp]
theorem Nat.mul_eq {x : Nat} {y : Nat} :
Nat.mul x y = x * y
source
@[simp]
theorem Nat.lt_eq {x : Nat} {y : Nat} :
Nat.lt x y = (x < y)
source
@[simp]
theorem Nat.le_eq {x : Nat} {y : Nat} :
Nat.le x y = (x ≤ y)
source
@[simp]
theorem Nat.zero_add (n : Nat) :
0 + n = n
source
theorem Nat.succ_add (n : Nat) (m : Nat) :
Nat.succ n + m = Nat.succ (n + m)
source
theorem Nat.add_succ (n : Nat) (m : Nat) :
n + Nat.succ m = Nat.succ (n + m)
source
theorem Nat.add_one (n : Nat) :
n + 1 = Nat.succ n
source
theorem Nat.succ_eq_add_one (n : Nat) :
Nat.succ n = n + 1
source
theorem Nat.add_comm (n : Nat) (m : Nat) :
n + m = m + n
source
theorem Nat.add_assoc (n : Nat) (m : Nat) (k : Nat) :
n + m + k = n + (m + k)
source
theorem Nat.add_left_comm (n : Nat) (m : Nat) (k : Nat) :
n + (m + k) = m + (n + k)
source
theorem Nat.add_right_comm (n : Nat) (m : Nat) (k : Nat) :
n + m + k = n + k + m
source
theorem Nat.add_left_cancel {n : Nat} {m : Nat} {k : Nat} :
n + m = n + k → m = k
source
theorem Nat.add_right_cancel {n : Nat} {m : Nat} {k : Nat} (h : n + m = k + m) :
n = k
source
@[simp]
theorem Nat.mul_zero (n : Nat) :
n * 0 = 0
source
theorem Nat.mul_succ (n : Nat) (m : Nat) :
n * Nat.succ m = n * m + n
source
@[simp]
theorem Nat.zero_mul (n : Nat) :
0 * n = 0
source
theorem Nat.succ_mul (n : Nat) (m : Nat) :
Nat.succ n * m = n * m + m
source
theorem Nat.mul_comm (n : Nat) (m : Nat) :
n * m = m * n
source
@[simp]
theorem Nat.mul_one (n : Nat) :
n * 1 = n
source
@[simp]
theorem Nat.one_mul (n : Nat) :
1 * n = n
source
theorem Nat.left_distrib (n : Nat) (m : Nat) (k : Nat) :
n * (m + k) = n * m + n * k
source
theorem Nat.right_distrib (n : Nat) (m : Nat) (k : Nat) :
(n + m) * k = n * k + m * k
source
theorem Nat.mul_add (n : Nat) (m : Nat) (k : Nat) :
n * (m + k) = n * m + n * k
source
theorem Nat.add_mul (n : Nat) (m : Nat) (k : Nat) :
(n + m) * k = n * k + m * k
source
theorem Nat.mul_assoc (n : Nat) (m : Nat) (k : Nat) :
n * m * k = n * (m * k)
source
theorem Nat.mul_left_comm (n : Nat) (m : Nat) (k : Nat) :
n * (m * k) = m * (n * k)
source
theorem Nat.succ_lt_succ {n : Nat} {m : Nat} :
n < m → Nat.succ n < Nat.succ m
source
theorem Nat.lt_succ_of_le {n : Nat} {m : Nat} :
n ≤ m → n < Nat.succ m
source
@[simp]
theorem Nat.sub_zero (n : Nat) :
n - 0 = n
source
theorem Nat.succ_sub_succ_eq_sub (n : Nat) (m : Nat) :
Nat.succ n - Nat.succ m = n - m
source
theorem Nat.pred_le (n : Nat) :
Nat.pred n ≤ n
source
theorem Nat.pred_lt {n : Nat} :
n ≠ 0 → Nat.pred n < n
source
theorem Nat.sub_le (n : Nat) (m : Nat) :
n - m ≤ n
source
theorem Nat.sub_lt {n : Nat} {m : Nat} :
0 < n → 0 < m → n - m < n
source
theorem Nat.sub_succ (n : Nat) (m : Nat) :
n - Nat.succ m = Nat.pred (n - m)
source
theorem Nat.succ_sub_succ (n : Nat) (m : Nat) :
Nat.succ n - Nat.succ m = n - m
source
theorem Nat.sub_self (n : Nat) :
n - n = 0
source
theorem Nat.lt_of_lt_of_le {n : Nat} {m : Nat} {k : Nat} :
n < m → m ≤ k → n < k
source
theorem Nat.lt_of_lt_of_eq {n : Nat} {m : Nat} {k : Nat} :
n < m → m = k → n < k
source
instance Nat.instTransNatLtInstLTNat :
Trans (fun a a_1 => a < a_1) (fun a a_1 => a < a_1) fun a a_1 => a < a_1
Equations
source
instance Nat.instTransNatLeInstLENat :
Trans (fun a a_1 => a ≤ a_1) (fun a a_1 => a ≤ a_1) fun a a_1 => a ≤ a_1
Equations
source
instance Nat.instTransNatLtInstLTNatLeInstLENat :
Trans (fun a a_1 => a < a_1) (fun a a_1 => a ≤ a_1) fun a a_1 => a < a_1
Equations
source
instance Nat.instTransNatLeInstLENatLtInstLTNat :
Trans (fun a a_1 => a ≤ a_1) (fun a a_1 => a < a_1) fun a a_1 => a < a_1
Equations
source
theorem Nat.le_of_eq {n : Nat} {m : Nat} (p : n = m) :
n ≤ m
source
theorem Nat.le_of_succ_le {n : Nat} {m : Nat} (h : Nat.succ n ≤ m) :
n ≤ m
source
theorem Nat.le_of_lt {n : Nat} {m : Nat} (h : n < m) :
n ≤ m
source
noncomputable def Nat.lt.step {n : Nat} {m : Nat} :
n < m → n < Nat.succ m
Equations
source
theorem Nat.eq_zero_or_pos (n : Nat) :
n = 0 ∨ n > 0
source
noncomputable def Nat.lt.base (n : Nat) :
n < Nat.succ n
Equations
source
theorem Nat.lt_succ_self (n : Nat) :
n < Nat.succ n
source
theorem Nat.le_total (m : Nat) (n : Nat) :
m ≤ n ∨ n ≤ m
source
theorem Nat.lt_of_le_and_ne {m : Nat} {n : Nat} (h₁ : m ≤ n) (h₂ : m ≠ n) :
m < n
source
theorem Nat.eq_zero_of_le_zero {n : Nat} (h : n ≤ 0) :
n = 0
source
theorem Nat.lt_of_succ_lt {n : Nat} {m : Nat} :
Nat.succ n < m → n < m
source
theorem Nat.lt_of_succ_lt_succ {n : Nat} {m : Nat} :
Nat.succ n < Nat.succ m → n < m
source
theorem Nat.lt_of_succ_le {n : Nat} {m : Nat} (h : Nat.succ n ≤ m) :
n < m
source
theorem Nat.succ_le_of_lt {n : Nat} {m : Nat} (h : n < m) :
Nat.succ n ≤ m
source
theorem Nat.zero_lt_of_lt {a : Nat} {b : Nat} :
a < b → 0 < b
source
theorem Nat.le_or_eq_or_le_succ {m : Nat} {n : Nat} (h : m ≤ Nat.succ n) :
m ≤ n ∨ m = Nat.succ n
source
theorem Nat.le_add_right (n : Nat) (k : Nat) :
n ≤ n + k
source
theorem Nat.le_add_left (n : Nat) (m : Nat) :
n ≤ m + n
source
theorem Nat.le.dest {n : Nat} {m : Nat} :
n ≤ m → ∃ k, n + k = m
source
theorem Nat.le.intro {n : Nat} {m : Nat} {k : Nat} (h : n + k = m) :
n ≤ m
source
theorem Nat.not_le_of_gt {n : Nat} {m : Nat} (h : n > m) :
¬n ≤ m
source
theorem Nat.gt_of_not_le {n : Nat} {m : Nat} (h : ¬n ≤ m) :
n > m
source
theorem Nat.add_le_add_left {n : Nat} {m : Nat} (h : n ≤ m) (k : Nat) :
k + n ≤ k + m
source
theorem Nat.add_le_add_right {n : Nat} {m : Nat} (h : n ≤ m) (k : Nat) :
n + k ≤ m + k
source
theorem Nat.add_lt_add_left {n : Nat} {m : Nat} (h : n < m) (k : Nat) :
k + n < k + m
source
theorem Nat.add_lt_add_right {n : Nat} {m : Nat} (h : n < m) (k : Nat) :
n + k < m + k
source
theorem Nat.zero_lt_one :
0 < 1
source
theorem Nat.add_le_add {a : Nat} {b : Nat} {c : Nat} {d : Nat} (h₁ : a ≤ b) (h₂ : c ≤ d) :
a + c ≤ b + d
source
theorem Nat.add_lt_add {a : Nat} {b : Nat} {c : Nat} {d : Nat} (h₁ : a < b) (h₂ : c < d) :
a + c < b + d
source
theorem Nat.ctor_eq_zero :
Nat.zero = 0
source
theorem Nat.one_ne_zero :
1 ≠ 0
source
theorem Nat.zero_ne_one :
0 ≠ 1
source
theorem Nat.succ_ne_zero (n : Nat) :
Nat.succ n ≠ 0
source
theorem Nat.mul_le_mul_left {n : Nat} {m : Nat} (k : Nat) (h : n ≤ m) :
k * n ≤ k * m
source
theorem Nat.mul_le_mul_right {n : Nat} {m : Nat} (k : Nat) (h : n ≤ m) :
n * k ≤ m * k
source
theorem Nat.mul_le_mul {n₁ : Nat} {m₁ : Nat} {n₂ : Nat} {m₂ : Nat} (h₁ : n₁ ≤ n₂) (h₂ : m₁ ≤ m₂) :
n₁ * m₁ ≤ n₂ * m₂
source
theorem Nat.mul_lt_mul_of_pos_left {n : Nat} {m : Nat} {k : Nat} (h : n < m) (hk : k > 0) :
k * n < k * m
source
theorem Nat.mul_lt_mul_of_pos_right {n : Nat} {m : Nat} {k : Nat} (h : n < m) (hk : k > 0) :
n * k < m * k
source
theorem Nat.mul_pos {n : Nat} {m : Nat} (ha : n > 0) (hb : m > 0) :
n * m > 0
source
theorem Nat.pow_succ (n : Nat) (m : Nat) :
n ^ Nat.succ m = n ^ m * n
source
theorem Nat.pow_zero (n : Nat) :
n ^ 0 = 1
source
theorem Nat.pow_le_pow_of_le_left {n : Nat} {m : Nat} (h : n ≤ m) (i : Nat) :
n ^ i ≤ m ^ i
source
theorem Nat.pow_le_pow_of_le_right {n : Nat} (hx : n > 0) {i : Nat} {j : Nat} :
i ≤ j → n ^ i ≤ n ^ j
source
theorem Nat.pos_pow_of_pos {n : Nat} (m : Nat) (h : 0 < n) :
0 < n ^ m
source
def Nat.min (n : Nat) (m : Nat) :
Nat
Equations
source
def Nat.max (n : Nat) (m : Nat) :
Nat
Equations
source
theorem Nat.not_eq_zero_of_lt {b : Nat} {a : Nat} (h : b < a) :
a ≠ 0
source
theorem Nat.pred_lt' {n : Nat} {m : Nat} (h : m < n) :
Nat.pred n < n
source
theorem Nat.add_sub_self_left (a : Nat) (b : Nat) :
a + b - a = b
source
theorem Nat.add_sub_self_right (a : Nat) (b : Nat) :
a + b - b = a
source
theorem Nat.sub_le_succ_sub (a : Nat) (i : Nat) :
a - i ≤ Nat.succ a - i
source
theorem Nat.zero_lt_sub_of_lt {i : Nat} {a : Nat} (h : i < a) :
0 < a - i
source
theorem Nat.sub_succ_lt_self (a : Nat) (i : Nat) (h : i < a) :
a - (i + 1) < a - i
source
@[inline]
def Prod.foldI {α : Type u} (f : Nat → α → α) (i : Nat × Nat) (a : α) :
α
Equations
source
@[inline]
def Prod.anyI (f : Nat → Bool) (i : Nat × Nat) :
Bool
Equations
source
@[inline]
def Prod.allI (f : Nat → Bool) (i : Nat × Nat) :
Bool
Equations