TensorPower — Mathlib

English

Homogeneous tensor powers M^{⊗ n} are defined as the tensor product over R indexed by Fin n, i.e., ⨂^n_R M ≔ ⨂[R] (i : Fin n), M.

Русский

Гомогенные тензорные степени M^{⊗ n} определяются как тензорное произведение над R, индексированное по Fin n, то есть ⨂^n_R M ≔ ⨂[R] (i : Fin n), M.

LaTeX

$$$M^{\\otimes n}_R \\;=\\; \\bigotimes_{i \\in \\mathrm{Fin}(n)} M,$$$

Lean4

/-- Homogeneous tensor powers $M^{\otimes n}$. `⨂[R]^n M` is a shorthand for
`⨂[R] (i : Fin n), M`. -/
abbrev TensorPower (R : Type*) (n : ℕ) (M : Type*) [CommSemiring R] [AddCommMonoid M] [Module R M] : Type _ :=
  ⨂[R] _ : Fin n, M

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