finFunctionFinEquiv_apply — Mathlib

English

For f: Fin n → Fin m, the canonical value of its image under the equivalence equals the sum over i of f(i) multiplied by m raised to i.

Русский

Для f: Fin n → Fin m, каноническое значение образа при преобразовании эквививалентности равно сумме по i от f(i) умноженного на m в степени i.

LaTeX

$$$$ (\\text{finFunctionFinEquiv } f : \\mathbb{N}) = \\sum_{i:\\mathrm{Fin} n} f(i) \\cdot m^{(i)}. $$$$

Lean4

theorem finFunctionFinEquiv_apply {m n : ℕ} (f : Fin n → Fin m) :
    (finFunctionFinEquiv f : ℕ) = ∑ i : Fin n, ↑(f i) * m ^ (i : ℕ) :=
  rfl

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