Commit 2024-03-01 13:29 c50fed87

View on Github →

chore: move Nat.repr_length to Data.Nat.Digits (#10511) There's no need to have this result so early. No changes to the moved code.

Estimated changes

Modified Mathlib/Data/Nat/Digits.lean

added theorem Nat.nat_repr_len_aux

added theorem Nat.repr_length

added theorem Nat.toDigitsCore_length

added theorem Nat.toDigitsCore_lens_eq

added theorem Nat.toDigitsCore_lens_eq_aux

Modified Mathlib/Init/Data/Nat/Lemmas.lean

deleted theorem Nat.nat_repr_len_aux

deleted theorem Nat.repr_length

deleted theorem Nat.toDigitsCore_length

deleted theorem Nat.toDigitsCore_lens_eq

deleted theorem Nat.toDigitsCore_lens_eq_aux