algebraMap_apply — Mathlib

English

Evaluating the product algebra map at index i yields the corresponding component algebra map.

Русский

При применении алгебраического отображения к произведению на индексi i получаем соответствующее отображение в координате i.

LaTeX

$$$ algebraMap_R (\\Pi i, A_i) a \\\\_i = algebraMap_R (A_i) a $$$

Lean4

@[simp]
theorem algebraMap_apply (a : R) (i : ι) : algebraMap R (Π i, A i) a i = algebraMap R (A i) a :=
  rfl

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