Theorem Nat.repr_length

Modification history

2024-03-01 13:29

Mathlib/Data/Nat/Digits.lean

chore: move Nat.repr_length to Data.Nat.Digits (#10511) …

Modified Nat.repr_length View on Github →

2022-06-23 18:33

Mathlib/Init/Data/Nat/Lemmas.lean

chore: fix unused variables from linter (#289) …

Modified Nat.repr_length View on Github →

2021-11-03 09:54

Mathlib/Init/Data/Nat/Lemmas.lean

feat(Init/Data/Nat/Lemmas); nat to string length lemmas (#77) …

Added Nat.repr_length View on Github →