mathlib documentation

data.nat.with_bot

with_bot #

Lemmas about the type of natural numbers with a bottom element adjoined.

theorem nat.with_bot.add_eq_zero_iff {n m : with_bot } :
n + m = 0 n = 0 m = 0
theorem nat.with_bot.add_eq_one_iff {n m : with_bot } :
n + m = 1 n = 0 m = 1 n = 1 m = 0
@[simp]
theorem nat.with_bot.coe_nonneg {n : } :
0 n
@[simp]
theorem nat.with_bot.lt_zero_iff (n : with_bot ) :
n < 0 n =