mapOfCompatibleSMul_tmul

Mathlib.LinearAlgebra.TensorProduct.Basic

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

English

The map preserves simple tensors exactly.

Русский

Отображение сохраняет простые тензоры точно.

LaTeX

$$$\\mathrm{mapOfCompatibleSMul}\\ R\\ A\\ M\\ N\\ (m \\otimes_A n) = m \\otimes_R n$$$

Lean4

@[simp]
theorem mapOfCompatibleSMul_tmul (m n) : mapOfCompatibleSMul R A M N (m ⊗ₜ n) = m ⊗ₜ n :=
  rfl

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

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

Разделы

Аффилиация

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