instSMul

Mathlib.LinearAlgebra.TensorProduct.Basic

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

English

There is an instance giving a scalar action of R on M ⊗_R N, i.e., the standard SMul on the tensor product.

Русский

Существует экземпляр, задающий действие скаляра R на M ⊗_R N — стандартное действие на тензорном произведении.

LaTeX

$$$ \\text{instance } \\mathrm{SMul}_{R} (M \\otimes_R N). $$$

Lean4

instance : SMul R (M ⊗[R] N) :=
  TensorProduct.leftHasSMul

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

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

Разделы

Аффилиация

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