Commit 2025-11-27 08:19 eee0187f

chore: remove obsolete NormDigits namespace (#30248) In Lean 3, nat.digits m n with concrete numbers m n could be normalized via norm_num. The logic enabling that was partially ported over to Lean 4 in the NormDigits namespace, but never was completed. Independently, simprocs as introduced in Lean v4.6.0 made it so that simp [Nat.digits, Nat.digitsAux] could normalize Nat.digits m n without any need for the special NormDigits code. More recently, #25864 made it so that just plain rfl can normalize Nat.digits m n (but note that a revert PR has been proposed in #30246). Therefore, the NormDigits namespace is no longer relevent and should be deleted.