coe_prod — Mathlib

English

The image of a product under the algebra map commutes with the product of images: the map preserves finite products of scalars from R to A and then to B.

Русский

Изображение произведения под алгебраMap сохраняет произведение изображений: отображение сохраняет конечные произведения скаляров из R в A и далее в B.

LaTeX

$$$\\big(\\prod_{i\\in s} a_i\\big)^{A} = \\prod_{i\\in s} (a_i)^{A}$$$

Lean4

@[norm_cast]
theorem coe_prod (a : ι → R) : (↑(∏ i ∈ s, a i : R) : A) = ∏ i ∈ s, (↑(a i) : A) :=
  map_prod (algebraMap R A) a s

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