Commit 2025-08-22 21:50 46b59734

View on Github →

chore(Data/Nat/Digits): deprecate coe_int_ofDigits (duplicate) (#28420)

Estimated changes

deleted theorem Nat.coe_int_ofDigits