finFunctionFinEquiv_single — Mathlib

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]

Похожие утверждения