Commit 2024-05-09 00:52 ba7e1146

View on Github →

feat(Data/Nat/Digits): digits_head and ofDigits_mod_eq_head (#11129)

Estimated changes

Modified Mathlib/Algebra/BigOperators/List/Basic.lean

Modified Mathlib/Computability/TMToPartrec.lean

Modified Mathlib/Data/List/Basic.lean

added theorem List.head!_nil

Modified Mathlib/Data/Nat/Defs.lean

added theorem Nat.default_eq_zero

Modified Mathlib/Data/Nat/Digits.lean

added theorem Nat.head!_digits

added theorem Nat.ofDigits_mod_eq_head!

added theorem Nat.ofDigits_nil