Commit 2023-01-02 21:50 da50f077

View on Github →

feat: port Data.Nat.WithBot (#1255)

Estimated changes

Modified Mathlib.lean

Created Mathlib/Data/Nat/WithBot.lean

added theorem Nat.WithBot.add_eq_one_iff

added theorem Nat.WithBot.add_eq_three_iff

added theorem Nat.WithBot.add_eq_two_iff

added theorem Nat.WithBot.add_eq_zero_iff

added theorem Nat.WithBot.coe_nonneg

added theorem Nat.WithBot.lt_one_iff_le_zero

added theorem Nat.WithBot.lt_zero_iff

added theorem Nat.WithBot.one_le_iff_zero_lt