How to prove mapping from n-ary number to nat is injective?

Stream: new members

[ptrl]

I have an idea of transforming it into a linear combination problem, but I’m not sure how to proceed with the transformation.
#mwe:

example {m n : ℕ} : Function.Injective (fun (a : Fin m → Fin n) => ∑i, (a i) * n^(i : ℕ)) := by sorry

m represents the number of digits.

[Eric Wieser]

I would use docs#finFunctionFinEquiv

[ptrl]

Eric Wieser said:

I would use docs#finFunctionFinEquiv

I will have a try! :+1:

[Junyan Xu]

I found Nat.digits_ofDigits when reviewing #18247. Maybe docs#finFunctionFinEquiv is also easier there ...