Note about deprecated files

This file is deprecated, and is no longer imported by anything in mathlib other than other deprecated files, and test files. You should not need to import it.

multiplication

@[deprecated Nat.mul_eq_zero]

theorem Nat.eq_zero_of_mul_eq_zero {m : ℕ} {n : ℕ} : n * m = 0 → n = 0 ∨ m = 0

Alias of the forward direction of Nat.mul_eq_zero.

successor and predecessor

@[deprecated]

def Nat.discriminate {B : Sort u} {n : ℕ} (H1 : n = 0 → B) (H2 : (m : ℕ) → n = m.succ → B) : B

Equations

• One or more equations did not get rendered due to their size.

@[deprecated]

theorem Nat.one_eq_succ_zero : 1 = Nat.succ 0

induction principles

@[deprecated]

def Nat.subInduction {P : ℕ → ℕ → Sort u} (H1 : (m : ℕ) → P 0 m) (H2 : (n : ℕ) → P n.succ 0) (H3 : (n m : ℕ) → P n m → P n.succ m.succ) (n : ℕ) (m : ℕ) : P n m

Equations

• Nat.subInduction H1 H2 H3 0 x = H1 x
• Nat.subInduction H1 H2 H3 _n.succ 0 = H2 _n
• Nat.subInduction H1 H2 H3 n.succ m.succ = H3 n m (Nat.subInduction H1 H2 H3 n m)

mod

@[deprecated]

theorem Nat.cond_decide_mod_two (x : ℕ) [d : Decidable (x % 2 = 1)] : (bif decide (x % 2 = 1) then 1 else 0) = x % 2