Finite-function digit numbering

Main results

• Nat.ofDigits_finFunctionFinEquiv: agreement with Mathlib's finite-function numbering.

The weighted-digit identity is the existing Nat.ofDigits_ofFn_eq_sum from fixed-length radix arithmetic; this module supplies only its bridge to Mathlib's finite-function enumeration.

theorem Nat.ofDigits_finFunctionFinEquiv {b L : ℕ} (f : Fin L → Fin b) : ofDigits b (List.ofFn fun (i : Fin L) => ↑(f i)) = ↑(finFunctionFinEquiv f)

finFunctionFinEquiv uses exactly ofDigits's least-significant-first convention.