map_comm

Mathlib.LinearAlgebra.TensorProduct.Basic

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

← MathLib Explorer

English

Range equality for the mapIncl construction.

Русский

Равенство образа для карты mapIncl.

LaTeX

$$$\\operatorname{range}(\\mathrm{mapIncl}\\ p\\ q) = \\mathrm{map_2}(\\mathrm{mk}\\ R\\ P\\ Q)\\ p\\ q$$$

Lean4

theorem map_comm (f : M →ₗ[R] P) (g : N →ₗ[R] Q) (x : N ⊗[R] M) :
    map f g (TensorProduct.comm R N M x) = TensorProduct.comm R Q P (map g f x) :=
  DFunLike.congr_fun (map_comp_comm_eq _ _) _

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

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

Разделы

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

Аффилиация

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