Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2023-07-11 12:40 3ed3f98a

View on Github →

feat(data/nat/order/basic): a + b - 1 ≤ a * b (#18737) and golf max_eq_zero_iff/min_eq_zero_iff To be used for Kneser's addition theorem.

Estimated changes

added theorem nat.add_sub_one_le_mul
modified theorem nat.max_eq_zero_iff
modified theorem nat.min_eq_zero_iff