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 (since := "2024-08-23")]

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 "No deprecation message was provided." (since := "2024-08-23")]

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.