ιMulti_apply — Mathlib

English

For any n and any v: Fin n → M, the value of ιMulti R n at v equals the product of ι_R(v(i)) over all i ∈ Fin n; i.e., ιMulti R n v = ∏_{i=0}^{n-1} ι_R(v(i)).

Русский

Для любого n и v: Fin n → M справедливо ιMulti R n v = ∏_{i=0}^{n-1} ι_R(v(i)).

LaTeX

$$$ ιMulti\\_R(n)(v) = \\prod_{i=0}^{n-1} ι_R(v(i)). $$$

Lean4

theorem ιMulti_apply {n : ℕ} (v : Fin n → M) : ιMulti R n v = (List.ofFn fun i => ι R (v i)).prod :=
  rfl

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