isEmptyEquiv_apply_tprod — Mathlib

English

Whenever the index is empty, the tensor product reduces to the base ring, giving a canonical evaluation map.

Русский

Если множество индексов пусто, тензорное произведение сводится к базовому кольцу, образуя каноническую оценку.

LaTeX

$$$\\text{isEmptyEquiv}: (⨂[R] i, s i) \\cong_R R$ with the map given by lifting the constant-1 tensor.$$

Lean4

@[simp]
theorem isEmptyEquiv_apply_tprod [IsEmpty ι] (f : Π i, s i) : isEmptyEquiv ι (tprod R f) = 1 :=
  lift.tprod _

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