single_tmul — Mathlib

English

Let Pi.single(i,m) be a pure tensor in the i-th slot. Then swapping the order gives Pi.single(i, m ⊗ x) at coordinate j equals Pi.single(i, m) at j tensored with x.

Русский

Пусть Pi.single(i,m) является чистым тензором в i–й позиции. Тогда pорядковая перестановка даёт Pi.single(i, m ⊗ x) в координате j равной Pi.single(i,m) в координате j, тензированному с x.

LaTeX

$$$ (\\Pi.single(i,m))_j \\otimes_R x = (\\Pi.single(i, m \\otimes_R x))_j. $$$

Lean4

theorem single_tmul {ι : Type*} [DecidableEq ι] {M : ι → Type*} [∀ i, AddCommMonoid (M i)] [∀ i, Module R (M i)] (i : ι)
    (x : N) (m : M i) (j : ι) : Pi.single i m j ⊗ₜ[R] x = (Pi.single i (m ⊗ₜ[R] x) : ∀ i, M i ⊗[R] N) j := by
  by_cases h : i = j <;> aesop

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