finPiFinEquiv_apply — Mathlib

English

For f: Fin m → Fin n, the image under the equivalence has a Nat-valued expression given by summing the products of f i and n(i) over Fin m.

Русский

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

LaTeX

$$$$ (finPiFinEquiv f).val = \\sum_{i: \\mathrm{Fin} m} f(i) \\cdot \\prod_{j} n (\\mathrm{Fin.castLE} i.is_lt.le j). $$$$

Lean4

theorem finPiFinEquiv_apply {m : ℕ} {n : Fin m → ℕ} (f : ∀ i : Fin m, Fin (n i)) :
    (finPiFinEquiv f : ℕ) = ∑ i, f i * ∏ j, n (Fin.castLE i.is_lt.le j) :=
  rfl

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