PiTensorProduct — Mathlib

English

PiTensorProduct R s is the tensor product of the family {s_i} indexed by i ∈ ι over the commutative semiring R.

Русский

PiTensorProduct R s есть тензорное произведение семейства модулей {s_i}, индексируемого по i ∈ ι, над кольцом-основанием R.

LaTeX

$$$\PiTensorProduct(R,s) \cong \bigotimes_{i\in \iota} s(i)$$$

Lean4

/-- `PiTensorProduct R s` with `R` a commutative semiring and `s : ι → Type*` is the tensor
  product of all the `s i`'s. This is denoted by `⨂[R] i, s i`. -/
def PiTensorProduct : Type _ :=
  (addConGen (PiTensorProduct.Eqv R s)).Quotient

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