mulRight_tmul — Mathlib

English

If one has a directed system of modules (F_i) with maps f_i^j, then the induced system on M ⊗_R F_i given by lTensor M (f_i^j) is directed.

Русский

Имея направленную систему модулей (F_i) с переходными отображениями, дается направленная система модулей M ⊗_R F_i с отображениями lTensor M (f_i^j).

LaTeX

$$$\\text{DirectedSystem}(F_i, f_i^j) \\Rightarrow\\ \\text{DirectedSystem}(M\\otimes_R F_i, lTensor\\,M\\, (f_i^j)).$$$

Lean4

theorem mulRight_tmul (a : A) (b : B) : mulRight R (a ⊗ₜ[R] b) = map (mulRight R a) (mulRight R b) := by ext; simp

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