sub_tmul

Mathlib.LinearAlgebra.TensorProduct.Basic

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

English

The map m ⊗ p respects subtraction in the first slot of the tensor product.

Русский

Отображение тензорного произведения сохраняет вычитание в первом аргументе.

LaTeX

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

Lean4

theorem sub_tmul (m₁ m₂ : M) (n : N) : (m₁ - m₂) ⊗ₜ n = m₁ ⊗ₜ[R] n - m₂ ⊗ₜ[R] n :=
  (mk R M N).map_sub₂ _ _ _

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

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

Разделы

Аффилиация

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