Theorem Nat.head!_digits

Modification history

2025-06-19 14:15

Mathlib/Data/Nat/Digits/Defs.lean

chore: split Data.Nat.Digits (#26134) …

Modified Nat.head!_digits View on Github →

2024-05-09 00:52

Mathlib/Data/Nat/Digits.lean

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

Added Nat.head!_digits View on Github →