Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2023-01-19 15:23 2609ad04

View on Github →

chore(data/nat/digits): golf, use seemingly weaker assumptions (#18203)

  • Golf.
  • Assume n ≠ 0 instead of 0 < n or 1 ≤ n.
  • Assume 1 < n instead of 2 ≤ n.
  • Add nat.exists_eq_add_of_le' (forward-ported in leanprover-community/mathlib4#1662).

Estimated changes

modified theorem nat.exists_eq_add_of_le
modified theorem nat.exists_eq_add_of_lt
modified theorem nat.digits_add
modified theorem nat.digits_def'
modified theorem nat.digits_last
modified theorem nat.digits_len
modified theorem nat.digits_lt_base
modified theorem nat.digits_of_lt
modified theorem nat.digits_zero_of_eq_zero
modified theorem nat.digits_zero_succ'