lTensor_comp_map

Mathlib.LinearAlgebra.TensorProduct.Basic

URI: https://scilib.ai/kg/mathlib#LinearMap.lTensor_comp_map

← MathLib Explorer

English

—

Русский

—

LaTeX

$$$$ (g'\!\,\mathrm{lTensor}\_)\!\circ \mathrm{map}\ f\ g = \mathrm{map}\ f\ (g'\circ g). $$$$

Lean4

@[simp]
theorem lTensor_comp_map (g' : Q →ₗ[R] S) (f : M →ₗ[R] P) (g : N →ₗ[R] Q) :
    (g'.lTensor _).comp (map f g) = map f (g'.comp g) := by simp only [lTensor, ← map_comp, id_comp]

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

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

Разделы

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

Аффилиация

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