tprod_apply — Mathlib

English

For n ∈ ℕ and x ∈ Fin n → M, the value of tprod_R M n x equals the product of the generators ι_R (x_i) in the tensor algebra.

Русский

Для натурального n и x ∈ Fin n → M значение tprod_R M n x равно произведению генераторов ι_R (x_i) в тензорной алгебре.

LaTeX

$$$\\forall n:\\, \\mathbb{N},\\; x:\\, \\mathrm{Fin}(n) \\to M,\\; tprod\\ R\\ M\\ n\\ x = \\prod_{i=0}^{n-1} ι_R(x(i))$$$

Lean4

@[simp]
theorem tprod_apply {n : ℕ} (x : Fin n → M) : tprod R M n x = (List.ofFn fun i => ι R (x i)).prod :=
  rfl

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