English
For m,n ∈ ℕ with m ≠ 0, and i ∈ Fin n, j ∈ Fin m, the equivalence applied to Pi.single(i,j) yields the natural number j times m^i.
Русский
Пусть m,n ∈ ℕ и m ≠ 0, i ∈ Fin n, j ∈ Fin m. Применение эквививалентности к Pi.single(i,j) даёт число j·m^i.
LaTeX
$$$$ (\\text{finFunctionFinEquiv} (\\Pi.single i j) : \\mathbb{N}) = j \\cdot m^{(i : \\mathbb{N})}. $$$$
Lean4
theorem finFunctionFinEquiv_single {m n : ℕ} [NeZero m] (i : Fin n) (j : Fin m) :
(finFunctionFinEquiv (Pi.single i j) : ℕ) = j * m ^ (i : ℕ) :=
by
rw [finFunctionFinEquiv_apply, Fintype.sum_eq_single i, Pi.single_eq_same]
rintro x hx
rw [Pi.single_eq_of_ne hx, Fin.val_zero, zero_mul]