constantBaseRingEquiv_tprod — Mathlib

English

The same base-ring identity as above specialized to the tprod construction: the image of tprod under constantBaseRingEquiv is the product ∏ i x_i.

Русский

Та же базовая тождественность для конструкций tprod: образ tprod под constantBaseRingEquiv равен произведению по индексам.

LaTeX

$$$constantBaseRingEquiv\\ ι\\ R\\ (tprod\\ R\\ x) = \\prod_i x_i$$$

Lean4

@[simp]
theorem constantBaseRingEquiv_tprod (x : ι → R) : constantBaseRingEquiv ι R (tprod R x) = ∏ i, x i := by
  simp [constantBaseRingEquiv]

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