Commit 2025-04-17 16:41 9ec5b5d8

View on Github →

feat: Nat.toDigits_length (#24126) Also generalize Nat.toDigitsCore_length.

Estimated changes

modified theorem Nat.repr_length
modified theorem Nat.toDigitsCore_length
added theorem Nat.toDigits_length