Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-11-25 14:56 f717251d

View on Github →

feat(data/nat/with_bot): add nat.with_bot.add_eq_iff lemmas (#17629)

Estimated changes

Modified src/data/nat/order/basic.lean

modified theorem nat.add_eq_one_iff

added theorem nat.add_eq_three_iff

added theorem nat.add_eq_two_iff

Modified src/data/nat/with_bot.lean

modified theorem nat.with_bot.add_eq_one_iff

added theorem nat.with_bot.add_eq_three_iff

added theorem nat.with_bot.add_eq_two_iff

modified theorem nat.with_bot.add_eq_zero_iff

modified theorem nat.with_bot.coe_nonneg

modified theorem nat.with_bot.lt_one_iff_le_zero

modified theorem nat.with_bot.lt_zero_iff

modified theorem nat.with_bot.one_le_iff_zero_lt