map_tmul

Mathlib.LinearAlgebra.TensorProduct.Tower

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

English

A lifting map evaluated on a simple tensor x ⊗ y equals the given bilinear map applied to x and y.

Русский

Лифтинг-отображение на простом тензоре x ⊗ y дает значение билинейного отображения на x и y.

LaTeX

$$$\text{lift}(f)(x \otimes_R y) = f(x)(y)$$$

Lean4

@[simp]
theorem map_tmul (f : M →ₗ[A] P) (g : N →ₗ[R] Q) (m : M) (n : N) : map f g (m ⊗ₜ n) = f m ⊗ₜ g n :=
  rfl

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

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

Разделы

Аффилиация

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