lidOfCompatibleSMul_tmul

Mathlib.LinearAlgebra.TensorProduct.Associator

URI: https://scilib.ai/kg/mathlib#TensorProduct.lidOfCompatibleSMul_tmul

English

The canonical A-linear map A ⊗R M → M sends a ⊗ m to the action a on m, i.e., a · m.

Русский

Каноническое A-линейное отображение A ⊗R M → M отправляет a ⊗ m в действие a над m, то есть a ⋅ m.

LaTeX

$$$\\mathrm{lidOfCompatibleSMul}\, R\, A\, M\\;(a\\otimes m) = a\\cdot m$$$

Lean4

theorem lidOfCompatibleSMul_tmul (a m) : lidOfCompatibleSMul R A M (a ⊗ₜ[R] m) = a • m :=
  rfl

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

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

Разделы

Аффилиация

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