tmul_sub

Mathlib.LinearAlgebra.TensorProduct.Basic

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

English

The tensor product is additive in the first component: (m1 - m2) ⊗ n equals (m1 ⊗ n) - (m2 ⊗ n).

Русский

Тензорное произведение аддитивно по первой компоненте.

LaTeX

$$$$(m_1 - m_2) \\otimes_R n = m_1 \\otimes_R n - m_2 \\otimes_R n.$$$$

Lean4

theorem tmul_sub (m : M) (p₁ p₂ : P) : m ⊗ₜ (p₁ - p₂) = m ⊗ₜ[R] p₁ - m ⊗ₜ[R] p₂ :=
  (mk R M P _).map_sub _ _

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

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

Разделы

Аффилиация

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