Commit 2024-02-20 08:45 300250f2

View on Github →

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

Estimated changes

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

added theorem Nat.toDigitsCore_length

added theorem Nat.toDigitsCore_lens_eq

added theorem Nat.toDigitsCore_lens_eq_aux

deleted theorem Nat.to_digits_core_length

deleted theorem Nat.to_digits_core_lens_eq

deleted theorem Nat.to_digits_core_lens_eq_aux