Commit 2026-03-19 04:12 3c0438ce

chore(Data/Nat/Digits): rename digits_len to digits_length (#36830) Rename Nat.digits_len to Nat.length_digits for consistency with the mathlib naming convention — the statement is about List.length (Nat.digits b n), so length_digits follows the standard projection-first pattern. Also renames:

• digits_len_le_digits_len_succ → length_digits_le_length_digits_succ
• le_digits_len_le → le_length_digits_le Deprecated aliases are added for backwards compatibility. Downstream files (e.g. Ostrowski.lean) are left unchanged since the deprecated aliases handle the transition. Addresses the Nat.digits_len item in #21584.

AI disclosure

I used Claude Code to explore the codebase (finding references, checking naming conventions) and to draft the PR description. I also used it to help with mechanical tasks like updating references across files and fixing lint issues. I reviewed and understand all changes — these are straightforward renames with deprecated aliases.