mulLeft_tmul

Mathlib.RingTheory.TensorProduct.Basic

URI: https://scilib.ai/kg/mathlib#LinearMap.mulLeft_tmul

English

Analogous equality for mulRight_tmul: mulRight on a ⊗ b equals map (mulRight a) (mulRight b).

Русский

Аналогично: mulRight на a ⊗ b равно map (mulRight a) (mulRight b).

LaTeX

$$$\\mathrm{mulRight}\\;R\\bigl(a\\otimes_R b\\bigr) = \\bigl(\\mathrm{map}(\\mathrm{mulRight}\\;R\\;a) (\\mathrm{mulRight}\\;R\\;b)\\bigr).$$$

Lean4

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

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru