Theorem Nat.length_digits_le_length_digits_succ

Modification history

2026-03-19 04:12
Mathlib/Data/Nat/Digits/Lemmas.lean
chore(Data/Nat/Digits): rename `digits_len` to `digits_length` (#36830) …
Added Nat.length_digits_le_length_digits_succView on Github →