tmul_single — Mathlib

English

Let i be an index, x ∈ N and m ∈ M_i. Then for every coordinate j, the j-th component of x ⊗ Π_single(i,m) equals the j-th component of Π_single(i, x ⊗ m).

Русский

Пусть i принадлежит индексу, x ∈ N и m ∈ M_i. Тогда для каждой координаты j равенство: j‑й компонент ∙(x ⊗ Π_single(i,m)) совпадает с j‑й компонентой Π_single(i, x ⊗ m).

LaTeX

$$$ (x \\otimes_R \\mathrm{Pi.single}(i,m))_j = (\\mathrm{Pi.single}(i, x \\otimes_R m))_j \\quad \\text{for all } j. $$$

Lean4

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

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