tmul_smul

Mathlib.LinearAlgebra.TensorProduct.Basic

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

← MathLib Explorer

English

Reiterating, the unit scalar on the tensor product acts as identity: 1 · x = x.

Русский

Еще раз: единичный скаляр действует как тождественный преобразователь: 1 · x = x.

LaTeX

$$$1 \cdot x = x$$$

Lean4

@[simp]
theorem tmul_smul [DistribMulAction R' N] [CompatibleSMul R R' M N] (r : R') (x : M) (y : N) :
    x ⊗ₜ (r • y) = r • x ⊗ₜ[R] y :=
  (smul_tmul _ _ _).symm

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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