cancelBaseChange_tmul

Mathlib.LinearAlgebra.TensorProduct.Tower

URI: https://scilib.ai/kg/mathlib#TensorProduct.AlgebraTensorModule.cancelBaseChange_tmul

English

The action of CancelBaseChange on a simple tensor m ⊗ (a ⊗ n) is (a • m) ⊗ n.

Русский

Действие CancelBaseChange на простой тензор m ⊗ (a ⊗ n): оно равно (a • m) ⊗ n.

LaTeX

$$$\mathrm{cancelBaseChange}(R,A,B,M,N)(m\otimes (a\otimes n)) = (a\cdot m)\otimes n$$$

Lean4

@[simp]
theorem cancelBaseChange_tmul (m : M) (n : N) (a : A) : cancelBaseChange R A B M N (m ⊗ₜ (a ⊗ₜ n)) = (a • m) ⊗ₜ n :=
  rfl

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

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

Разделы

Аффилиация

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