Theorem Nat.toDigitsCore_lens_eq_aux

Modification history

2024-03-01 13:29

Mathlib/Data/Nat/Digits.lean

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

Modified Nat.toDigitsCore_lens_eq_aux View on Github →

2024-02-20 08:45

Mathlib/Init/Data/Nat/Lemmas.lean

chore(Init/Data/Nat/Lemmas): rename 3 lemmata (#10730)

Added Nat.toDigitsCore_lens_eq_aux View on Github →