Commit 2025-10-05 11:42 34812cd2

View on Github →

feat(Nat/Digits): use fuel in Nat.digits (#25864) Add a fuel parameter to Nat.digitsAux to make it structurally recursive.

Estimated changes

Modified Mathlib/Data/Nat/Digits/Defs.lean

added theorem Nat.digitsAux.go_fuel_irrel

added theorem Nat.digitsAux.go_succ

added theorem Nat.digitsAux.go_zero

modified def Nat.digitsAux

modified theorem Nat.digitsAux_zero